[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
⊢ RingHom.comp (frobenius R p) ↑(RingEquiv.symm (frobeniusEquiv R p)) = RingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ↑(RingHom.comp (frobenius R p) ↑(RingEquiv.symm (frobeniusEquiv R p))) x✝ = ↑(RingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
⊢ RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p))) (frobenius R p) = RingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ↑(RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p))) (frobenius R p)) x✝ = ↑(RingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ↑(expand R p) f = map (↑(RingEquiv.symm (frobeniusEquiv R p))) f ^ p
[PROOFSTEP]
rw [← (f.map (S := R) (frobeniusEquiv R p).symm).expand_char p, map_expand, map_map, frobenius_comp_frobeniusEquiv_symm,
  map_id]
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible (↑(expand R p) f)
[PROOFSTEP]
have hp : Fact p.Prime := inferInstance
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
hp : Fact (Nat.Prime p)
⊢ ¬Irreducible (↑(expand R p) f)
[PROOFSTEP]
rw [polynomial_expand_eq]
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
hp : Fact (Nat.Prime p)
⊢ ¬Irreducible (map (↑(RingEquiv.symm (frobeniusEquiv R p))) f ^ p)
[PROOFSTEP]
exact fun hf ↦ hf.not_unit $ (of_irreducible_pow hp.out.ne_one hf).pow p
[GOAL]
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
⊢ PerfectRing (R × S) p
[PROOFSTEP]
constructor
[GOAL]
case bijective_frobenius
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
⊢ Bijective ↑(frobenius (R × S) p)
[PROOFSTEP]
have : frobenius (R × S) p = Prod.map (frobenius R p) (frobenius S p) := by ext <;> simp [frobenius_def]
[GOAL]
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
⊢ ↑(frobenius (R × S) p) = Prod.map ↑(frobenius R p) ↑(frobenius S p)
[PROOFSTEP]
ext
[GOAL]
case h.h₁
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
x✝ : R × S
⊢ (↑(frobenius (R × S) p) x✝).fst = (Prod.map (↑(frobenius R p)) (↑(frobenius S p)) x✝).fst
[PROOFSTEP]
simp [frobenius_def]
[GOAL]
case h.h₂
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
x✝ : R × S
⊢ (↑(frobenius (R × S) p) x✝).snd = (Prod.map (↑(frobenius R p)) (↑(frobenius S p)) x✝).snd
[PROOFSTEP]
simp [frobenius_def]
[GOAL]
case bijective_frobenius
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
this : ↑(frobenius (R × S) p) = Prod.map ↑(frobenius R p) ↑(frobenius S p)
⊢ Bijective ↑(frobenius (R × S) p)
[PROOFSTEP]
rw [this]
[GOAL]
case bijective_frobenius
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
this : ↑(frobenius (R × S) p) = Prod.map ↑(frobenius R p) ↑(frobenius S p)
⊢ Bijective (Prod.map ↑(frobenius R p) ↑(frobenius S p))
[PROOFSTEP]
exact Bijective.Prod_map (bijective_frobenius R p) (bijective_frobenius S p)
[GOAL]
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
⊢ PerfectField K
[PROOFSTEP]
refine' PerfectField.mk $ fun hf ↦ _
[GOAL]
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
f✝ : K[X]
hf : Irreducible f✝
⊢ Separable f✝
[PROOFSTEP]
rcases separable_or p hf with h | ⟨-, g, -, rfl⟩
[GOAL]
case inl
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
f✝ : K[X]
hf : Irreducible f✝
h : Separable f✝
⊢ Separable f✝
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.intro.intro
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
g : K[X]
hf : Irreducible (↑(expand K p) g)
⊢ Separable (↑(expand K p) g)
[PROOFSTEP]
exfalso
[GOAL]
case inr.intro.intro.intro.h
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
g : K[X]
hf : Irreducible (↑(expand K p) g)
⊢ False
[PROOFSTEP]
revert hf
[GOAL]
case inr.intro.intro.intro.h
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
g : K[X]
⊢ Irreducible (↑(expand K p) g) → False
[PROOFSTEP]
simp
[GOAL]
K : Type ?u.469717
inst✝¹ : Field K
inst✝ : Finite K
⊢ PerfectField K
[PROOFSTEP]
obtain ⟨p, _instP⟩ := CharP.exists K
[GOAL]
case intro
K : Type ?u.469717
inst✝¹ : Field K
inst✝ : Finite K
p : ℕ
_instP : CharP K p
⊢ PerfectField K
[PROOFSTEP]
have : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
[GOAL]
case intro
K : Type ?u.469717
inst✝¹ : Field K
inst✝ : Finite K
p : ℕ
_instP : CharP K p
this : Fact (Nat.Prime p)
⊢ PerfectField K
[PROOFSTEP]
exact PerfectRing.toPerfectField K p
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ PerfectRing K p
[PROOFSTEP]
refine' PerfectRing.ofSurjective _ _ $ fun y ↦ _
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let f : K[X] := X ^ p - C y
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let L := f.SplittingField
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let ι := algebraMap K L
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
have hf_deg : f.degree ≠ 0 := by rw [degree_X_pow_sub_C hp.out.pos y, p.cast_ne_zero]; exact hp.out.ne_zero
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
⊢ degree f ≠ 0
[PROOFSTEP]
rw [degree_X_pow_sub_C hp.out.pos y, p.cast_ne_zero]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
⊢ p ≠ 0
[PROOFSTEP]
exact hp.out.ne_zero
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let a : L := f.rootOfSplits ι (SplittingField.splits f) hf_deg
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
have hfa : aeval a f = 0 := by rw [aeval_def, map_rootOfSplits _ (SplittingField.splits f) hf_deg]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
⊢ ↑(aeval a) f = 0
[PROOFSTEP]
rw [aeval_def, map_rootOfSplits _ (SplittingField.splits f) hf_deg]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
have ha_pow : a ^ p = ι y := by rwa [AlgHom.map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hfa 
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
⊢ a ^ p = ↑ι y
[PROOFSTEP]
rwa [AlgHom.map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hfa 
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let g : K[X] := minpoly K a
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
suffices : (g.map ι).natDegree = 1
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : natDegree (map ι g) = 1
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
rw [g.natDegree_map, ← degree_eq_iff_natDegree_eq_of_pos Nat.one_pos] at this 
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : degree g = ↑1
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
obtain ⟨a' : K, ha' : ι a' = a⟩ := minpoly.mem_range_of_degree_eq_one K a this
[GOAL]
case intro
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : degree g = ↑1
a' : K
ha' : ↑ι a' = a
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
refine' ⟨a', NoZeroSMulDivisors.algebraMap_injective K L _⟩
[GOAL]
case intro
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : degree g = ↑1
a' : K
ha' : ↑ι a' = a
⊢ ↑(algebraMap K L) (↑(frobenius K p) a') = ↑(algebraMap K L) y
[PROOFSTEP]
rw [RingHom.map_frobenius, ha', frobenius_def, ha_pow]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have hg_dvd : g.map ι ∣ (X - C a) ^ p :=
  by
  convert Polynomial.map_dvd ι (minpoly.dvd K a hfa)
  rw [sub_pow_char, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ map ι g ∣ (X - ↑C a) ^ p
[PROOFSTEP]
convert Polynomial.map_dvd ι (minpoly.dvd K a hfa)
[GOAL]
case h.e'_4
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ (X - ↑C a) ^ p = map ι f
[PROOFSTEP]
rw [sub_pow_char, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have ha : IsIntegral K a := isIntegral_of_finite K a
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have hg_pow : g.map ι = (X - C a) ^ (g.map ι).natDegree :=
  by
  obtain ⟨q, -, hq⟩ := (dvd_prime_pow (prime_X_sub_C a) p).mp hg_dvd
  rw [eq_of_monic_of_associated ((minpoly.monic ha).map ι) ((monic_X_sub_C a).pow q) hq, natDegree_pow,
    natDegree_X_sub_C, mul_one]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
⊢ map ι g = (X - ↑C a) ^ natDegree (map ι g)
[PROOFSTEP]
obtain ⟨q, -, hq⟩ := (dvd_prime_pow (prime_X_sub_C a) p).mp hg_dvd
[GOAL]
case intro.intro
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
q : ℕ
hq : Associated (map ι g) ((X - ↑C a) ^ q)
⊢ map ι g = (X - ↑C a) ^ natDegree (map ι g)
[PROOFSTEP]
rw [eq_of_monic_of_associated ((minpoly.monic ha).map ι) ((monic_X_sub_C a).pow q) hq, natDegree_pow, natDegree_X_sub_C,
  mul_one]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have hg_sep : (g.map ι).Separable := (separable_of_irreducible $ minpoly.irreducible ha).map
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable (map ι g)
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
rw [hg_pow] at hg_sep 
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable ((X - ↑C a) ^ natDegree (map ι g))
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
refine' (Separable.of_pow (not_isUnit_X_sub_C a) _ hg_sep).2
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable ((X - ↑C a) ^ natDegree (map ι g))
⊢ natDegree (map ι g) ≠ 0
[PROOFSTEP]
rw [g.natDegree_map ι, ← Nat.pos_iff_ne_zero, natDegree_pos_iff_degree_pos]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable ((X - ↑C a) ^ natDegree (map ι g))
⊢ 0 < degree g
[PROOFSTEP]
exact minpoly.degree_pos ha
