[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
h : Separable p
⊢ Splits f p
[PROOFSTEP]
convert IsSepClosed.splits_of_separable (p.map f) (Separable.map h)
[GOAL]
case a
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
h : Separable p
⊢ Splits f p ↔ Splits (RingHom.id K) (map f p)
[PROOFSTEP]
simp [splits_map_iff]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
have hn' : 0 < n :=
  Nat.pos_of_ne_zero <| fun h => by
    rw [h, Nat.cast_zero] at hn 
    exact hn.out rfl
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
h : n = 0
⊢ False
[PROOFSTEP]
rw [h, Nat.cast_zero] at hn 
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero 0
h : n = 0
⊢ False
[PROOFSTEP]
exact hn.out rfl
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
have : degree (X ^ n - C x) ≠ 0 := by
  rw [degree_X_pow_sub_C hn' x]
  exact (WithBot.coe_lt_coe.2 hn').ne'
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ degree (X ^ n - ↑C x) ≠ 0
[PROOFSTEP]
rw [degree_X_pow_sub_C hn' x]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact (WithBot.coe_lt_coe.2 hn').ne'
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : x = 0
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
exact ⟨0, by rw [hx, pow_eq_zero_iff hn']⟩
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : x = 0
⊢ 0 ^ n = x
[PROOFSTEP]
rw [hx, pow_eq_zero_iff hn']
[GOAL]
case neg
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : ¬x = 0
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx
[GOAL]
case neg.intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : ¬x = 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
use z
[GOAL]
case h
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : ¬x = 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ z ^ n = x
[PROOFSTEP]
simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def, sub_eq_zero] using hz
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
h2 : NeZero 2
⊢ ∃ z, x = z * z
[PROOFSTEP]
rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩
[GOAL]
case intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
h2 : NeZero 2
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
[PROOFSTEP]
exact ⟨z, sq z⟩
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
⊢ roots p = 0 ↔ p = ↑C (coeff p 0)
[PROOFSTEP]
refine' ⟨fun h => _, fun hp => by rw [hp, roots_C]⟩
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
hp : p = ↑C (coeff p 0)
⊢ roots p = 0
[PROOFSTEP]
rw [hp, roots_C]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
cases' le_or_lt (degree p) 0 with hd hd
[GOAL]
case inl
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : degree p ≤ 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
exact eq_C_of_degree_le_zero hd
[GOAL]
case inr
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : 0 < degree p
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
obtain ⟨z, hz⟩ := IsSepClosed.exists_root p hd.ne' hsep
[GOAL]
case inr.intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : 0 < degree p
z : k
hz : IsRoot p z
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz 
[GOAL]
case inr.intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : 0 < degree p
z : k
hz : z ∈ 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
simp at hz 
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
hp : degree p ≠ 0
hsep : Separable p
⊢ degree (map f p) ≠ 0
[PROOFSTEP]
rwa [degree_map_eq_of_injective f.injective]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
hp : degree p ≠ 0
hsep : Separable p
x : K
hx : IsRoot (map f p) x
⊢ eval₂ f x p = 0
[PROOFSTEP]
rwa [eval₂_eq_eval_map, ← IsRoot]
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
⊢ IsSepClosed k
[PROOFSTEP]
refine ⟨fun p hsep ↦ Or.inr ?_⟩
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → degree g = 1
[PROOFSTEP]
intro q hq hdvd
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ map (RingHom.id k) p
⊢ degree q = 1
[PROOFSTEP]
simp only [map_id] at hdvd 
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
⊢ degree q = 1
[PROOFSTEP]
have hlc : IsUnit (leadingCoeff q)⁻¹ := IsUnit.inv <| Ne.isUnit <| leadingCoeff_ne_zero.2 <| Irreducible.ne_zero hq
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
⊢ degree q = 1
[PROOFSTEP]
have hsep' : Separable (q * C (leadingCoeff q)⁻¹) :=
  Separable.mul (Separable.of_dvd hsep hdvd) ((separable_C _).2 hlc)
    (by simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul] using isCoprime_one_right (x := q))
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
⊢ IsCoprime q (↑C (leadingCoeff q)⁻¹)
[PROOFSTEP]
simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul] using isCoprime_one_right (x := q)
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
⊢ degree q = 1
[PROOFSTEP]
have hirr' := hq
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
hirr' : Irreducible q
⊢ degree q = 1
[PROOFSTEP]
rw [← irreducible_mul_isUnit (isUnit_C.2 hlc)] at hirr' 
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
hirr' : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
⊢ degree q = 1
[PROOFSTEP]
obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) hirr' hsep'
[GOAL]
case intro
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
hirr' : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
x : k
hx : eval x (q * ↑C (leadingCoeff q)⁻¹) = 0
⊢ degree q = 1
[PROOFSTEP]
exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root hirr' hx
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
⊢ Function.Surjective ↑(algebraMap k K)
[PROOFSTEP]
refine fun x => ⟨-(minpoly k x).coeff 0, ?_⟩
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (IsSeparable.isIntegral k x)
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have hsep : (minpoly k x).Separable := IsSeparable.separable k x
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have h : (minpoly k x).degree = 1 :=
  degree_eq_one_of_irreducible k (minpoly.irreducible (IsSeparable.isIntegral k x)) hsep
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
h : degree (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
h : degree (minpoly k x) = 1
this : ↑(aeval x) (minpoly k x) = 0
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C, add_eq_zero_iff_eq_neg] at this 
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
h : degree (minpoly k x) = 1
this : x = -↑(algebraMap k K) (coeff (minpoly k x) 0)
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
[GOAL]
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
⊢ IsAlgebraic k x
[PROOFSTEP]
apply IsIntegral.isAlgebraic
[GOAL]
case a
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
⊢ IsIntegral k x
[PROOFSTEP]
exact IsSepClosure.separable.isIntegral' x
[GOAL]
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
⊢ Separable (minpoly k x)
[PROOFSTEP]
have : IsSeparable k K := IsSepClosure.separable
[GOAL]
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
this : IsSeparable k K
⊢ Separable (minpoly k x)
[PROOFSTEP]
exact IsSeparable.separable k x
