refactor(FieldTheory/KummerExtension): Split off irreducibility of X ^ p - a (#20695)

This PR splits of irreducibility of `X ^ p - a` from `FieldTheory/KummerExtension` since it has lighter imports and can be used to golf a proof in `FieldTheory/Perfect`.



Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Author: tb65536

Mathlib.lean

@@ -3103,6 +3103,7 @@ import Mathlib.FieldTheory.Isaacs
 import Mathlib.FieldTheory.JacobsonNoether
 import Mathlib.FieldTheory.KrullTopology
 import Mathlib.FieldTheory.KummerExtension
+import Mathlib.FieldTheory.KummerPolynomial
 import Mathlib.FieldTheory.Laurent
 import Mathlib.FieldTheory.LinearDisjoint
 import Mathlib.FieldTheory.Minpoly.Basic

Mathlib/FieldTheory/KummerExtension.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
-import Mathlib.RingTheory.AdjoinRoot
 import Mathlib.FieldTheory.Galois.Basic
+import Mathlib.FieldTheory.KummerPolynomial
 import Mathlib.LinearAlgebra.Eigenspace.Minpoly
 import Mathlib.RingTheory.Norm.Basic
 /-!
@@ -31,8 +31,6 @@ then isomorphic to `Multiplicative (ZMod n)` whose inverse is given by
 
 ## Other results
 Criteria for `X ^ n - C a` to be irreducible is given:
-- `X_pow_sub_C_irreducible_iff_of_prime`:
-  For `n = p` a prime, `X ^ n - C a` is irreducible iff `a` is not a `p`-power.
 - `X_pow_sub_C_irreducible_iff_of_prime_pow`:
   For `n = p ^ k` an odd prime power, `X ^ n - C a` is irreducible iff `a` is not a `p`-power.
 - `X_pow_sub_C_irreducible_iff_forall_prime_of_odd`:
@@ -51,26 +49,6 @@ open Polynomial IntermediateField AdjoinRoot
 
 section Splits
 
-lemma root_X_pow_sub_C_pow (n : ℕ) (a : K) :
-    (AdjoinRoot.root (X ^ n - C a)) ^ n = AdjoinRoot.of _ a := by
-  rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]
-
-lemma root_X_pow_sub_C_ne_zero {n : ℕ} (hn : 1 < n) (a : K) :
-    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 :=
-  mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.not_eq_zero_of_lt hn))
-    X_ne_zero <| by rwa [natDegree_X_pow_sub_C, natDegree_X]
-
-lemma root_X_pow_sub_C_ne_zero' {n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) :
-    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 := by
-  obtain (rfl|hn) := (Nat.succ_le_iff.mpr hn).eq_or_lt
-  · rw [pow_one]
-    intro e
-    refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_
-    trans AdjoinRoot.mk (X - C a) (X - (X - C a))
-    · rw [sub_sub_cancel]
-    · rw [map_sub, mk_self, sub_zero, mk_X, e]
-  · exact root_X_pow_sub_C_ne_zero hn a
-
 theorem X_pow_sub_C_splits_of_isPrimitiveRoot
     {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α a : K} (e : α ^ n = a) :
     (X ^ n - C a).Splits (RingHom.id _) := by
@@ -105,85 +83,6 @@ end Splits
 
 section Irreducible
 
-lemma ne_zero_of_irreducible_X_pow_sub_C {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
-    n ≠ 0 := by
-  rintro rfl
-  rw [pow_zero, ← C.map_one, ← map_sub] at H
-  exact not_irreducible_C _ H
-
-lemma ne_zero_of_irreducible_X_pow_sub_C' {n : ℕ} (hn : n ≠ 1) {a : K}
-    (H : Irreducible (X ^ n - C a)) : a ≠ 0 := by
-  rintro rfl
-  rw [map_zero, sub_zero] at H
-  exact not_irreducible_pow hn H
-
-lemma root_X_pow_sub_C_eq_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
-    (AdjoinRoot.root (X ^ n - C a)) = 0 ↔ a = 0 := by
-  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-  refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
-  rintro rfl
-  have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
-  rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
-
-lemma root_X_pow_sub_C_ne_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
-    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 ↔ a ≠ 0 :=
-  (root_X_pow_sub_C_eq_zero_iff H).not
-
-theorem pow_ne_of_irreducible_X_pow_sub_C {n : ℕ} {a : K}
-    (H : Irreducible (X ^ n - C a)) {m : ℕ} (hm : m ∣ n) (hm' : m ≠ 1) (b : K) : b ^ m ≠ a := by
-  have hn : n ≠ 0 := fun e ↦ not_irreducible_C
-    (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)
-  obtain ⟨k, rfl⟩ := hm
-  rintro rfl
-  obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m
-  rw [mul_comm, pow_mul, map_pow, hq] at H
-  have : degree q = 0 := by
-    simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
-      Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 _ q rfl
-  apply_fun degree at hq
-  simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
-    Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero,
-    Nat.cast_injective.eq_iff] at hq
-  exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)
-
-/--Let `p` be a prime number. Let `K` be a field.
-Let `t ∈ K` be an element which does not have a `p`th root in `K`.
-Then the polynomial `x ^ p - t` is irreducible over `K`.-/
-@[stacks 09HF "We proved the result without the condition that `K` is char p in 09HF."]
-theorem X_pow_sub_C_irreducible_of_prime {p : ℕ} (hp : p.Prime) {a : K} (ha : ∀ b : K, b ^ p ≠ a) :
-    Irreducible (X ^ p - C a) := by
-  -- First of all, We may find an irreducible factor `g` of `X ^ p - C a`.
-  have : ¬ IsUnit (X ^ p - C a) := by
-    rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
-    exact hp.ne_zero
-  have ⟨g, hg, hg'⟩ := WfDvdMonoid.exists_irreducible_factor this (X_pow_sub_C_ne_zero hp.pos a)
-  -- It suffices to show that `deg g = p`.
-  suffices natDegree g = p from (associated_of_dvd_of_natDegree_le hg'
-    (X_pow_sub_C_ne_zero hp.pos a) (this.trans natDegree_X_pow_sub_C.symm).ge).irreducible hg
-  -- Suppose `deg g ≠ p`.
-  by_contra h
-  have : Fact (Irreducible g) := ⟨hg⟩
-  -- Let `r` be a root of `g`, then `N_K(r) ^ p = N_K(r ^ p) = N_K(a) = a ^ (deg g)`.
-  have key : (Algebra.norm K (AdjoinRoot.root g)) ^ p = a ^ g.natDegree := by
-    have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
-    rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
-    rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
-      ← finrank_top', ← IntermediateField.adjoin_root_eq_top g,
-      IntermediateField.adjoin.finrank,
-      AdjoinRoot.minpoly_root hg.ne_zero, natDegree_mul_C]
-    · simpa using hg.ne_zero
-    · exact AdjoinRoot.isIntegral_root hg.ne_zero
-  -- Since `a ^ (deg g)` is a `p`-power, and `p` is coprime to `deg g`, we conclude that `a` is
-  -- also a `p`-power, contradicting the hypothesis
-  have : p.Coprime (natDegree g) := hp.coprime_iff_not_dvd.mpr (fun e ↦ h (((natDegree_le_of_dvd hg'
-    (X_pow_sub_C_ne_zero hp.pos a)).trans_eq natDegree_X_pow_sub_C).antisymm (Nat.le_of_dvd
-      (natDegree_pos_iff_degree_pos.mpr <| Polynomial.degree_pos_of_irreducible hg) e)))
-  exact ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec
-
-theorem X_pow_sub_C_irreducible_iff_of_prime {p : ℕ} (hp : p.Prime) {a : K} :
-    Irreducible (X ^ p - C a) ↔ ∀ b, b ^ p ≠ a :=
-  ⟨(pow_ne_of_irreducible_X_pow_sub_C · dvd_rfl hp.ne_one), X_pow_sub_C_irreducible_of_prime hp⟩
-
 theorem X_pow_mul_sub_C_irreducible
     {n m : ℕ} {a : K} (hm : Irreducible (X ^ m - C a))
     (hn : ∀ (E : Type u) [Field E] [Algebra K E] (x : E) (_ : minpoly K x = X ^ m - C a),

Mathlib/FieldTheory/KummerPolynomial.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2023 Andrew Yang, Patrick Lutz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.AdjoinRoot
+import Mathlib.RingTheory.Norm.Defs
+/-!
+# Irreducibility of X ^ p - a
+
+## Main result
+- `X_pow_sub_C_irreducible_iff_of_prime`: For `p` prime, `X ^ p - C a` is irreducible iff `a` is not
+  a `p`-power. This is not true for composite `n`. For example, `x^4+4=(x^2-2x+2)(x^2+2x+2)` but
+  `-4` is not a 4th power.
+
+-/
+universe u
+
+variable {K : Type u} [Field K]
+
+open Polynomial AdjoinRoot
+
+section Splits
+
+lemma root_X_pow_sub_C_pow (n : ℕ) (a : K) :
+    (AdjoinRoot.root (X ^ n - C a)) ^ n = AdjoinRoot.of _ a := by
+  rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]
+
+lemma root_X_pow_sub_C_ne_zero {n : ℕ} (hn : 1 < n) (a : K) :
+    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 :=
+  mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.not_eq_zero_of_lt hn))
+    X_ne_zero <| by rwa [natDegree_X_pow_sub_C, natDegree_X]
+
+lemma root_X_pow_sub_C_ne_zero' {n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) :
+    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 := by
+  obtain (rfl|hn) := (Nat.succ_le_iff.mpr hn).eq_or_lt
+  · rw [pow_one]
+    intro e
+    refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_
+    trans AdjoinRoot.mk (X - C a) (X - (X - C a))
+    · rw [sub_sub_cancel]
+    · rw [map_sub, mk_self, sub_zero, mk_X, e]
+  · exact root_X_pow_sub_C_ne_zero hn a
+
+end Splits
+
+section Irreducible
+
+lemma ne_zero_of_irreducible_X_pow_sub_C {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
+    n ≠ 0 := by
+  rintro rfl
+  rw [pow_zero, ← C.map_one, ← map_sub] at H
+  exact not_irreducible_C _ H
+
+lemma ne_zero_of_irreducible_X_pow_sub_C' {n : ℕ} (hn : n ≠ 1) {a : K}
+    (H : Irreducible (X ^ n - C a)) : a ≠ 0 := by
+  rintro rfl
+  rw [map_zero, sub_zero] at H
+  exact not_irreducible_pow hn H
+
+lemma root_X_pow_sub_C_eq_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
+    (AdjoinRoot.root (X ^ n - C a)) = 0 ↔ a = 0 := by
+  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
+  refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
+  rintro rfl
+  have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
+  rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
+
+lemma root_X_pow_sub_C_ne_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
+    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 ↔ a ≠ 0 :=
+  (root_X_pow_sub_C_eq_zero_iff H).not
+
+theorem pow_ne_of_irreducible_X_pow_sub_C {n : ℕ} {a : K}
+    (H : Irreducible (X ^ n - C a)) {m : ℕ} (hm : m ∣ n) (hm' : m ≠ 1) (b : K) : b ^ m ≠ a := by
+  have hn : n ≠ 0 := fun e ↦ not_irreducible_C
+    (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)
+  obtain ⟨k, rfl⟩ := hm
+  rintro rfl
+  obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m
+  rw [mul_comm, pow_mul, map_pow, hq] at H
+  have : degree q = 0 := by
+    simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
+      Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 _ q rfl
+  apply_fun degree at hq
+  simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
+    Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero,
+    Nat.cast_injective.eq_iff] at hq
+  exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)
+
+/--Let `p` be a prime number. Let `K` be a field.
+Let `t ∈ K` be an element which does not have a `p`th root in `K`.
+Then the polynomial `x ^ p - t` is irreducible over `K`.-/
+@[stacks 09HF "We proved the result without the condition that `K` is char p in 09HF."]
+theorem X_pow_sub_C_irreducible_of_prime {p : ℕ} (hp : p.Prime) {a : K} (ha : ∀ b : K, b ^ p ≠ a) :
+    Irreducible (X ^ p - C a) := by
+  -- First of all, We may find an irreducible factor `g` of `X ^ p - C a`.
+  have : ¬ IsUnit (X ^ p - C a) := by
+    rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
+    exact hp.ne_zero
+  have ⟨g, hg, hg'⟩ := WfDvdMonoid.exists_irreducible_factor this (X_pow_sub_C_ne_zero hp.pos a)
+  -- It suffices to show that `deg g = p`.
+  suffices natDegree g = p from (associated_of_dvd_of_natDegree_le hg'
+    (X_pow_sub_C_ne_zero hp.pos a) (this.trans natDegree_X_pow_sub_C.symm).ge).irreducible hg
+  -- Suppose `deg g ≠ p`.
+  by_contra h
+  have : Fact (Irreducible g) := ⟨hg⟩
+  -- Let `r` be a root of `g`, then `N_K(r) ^ p = N_K(r ^ p) = N_K(a) = a ^ (deg g)`.
+  have key : (Algebra.norm K (AdjoinRoot.root g)) ^ p = a ^ g.natDegree := by
+    have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
+    rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
+    rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
+      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
+  -- Since `a ^ (deg g)` is a `p`-power, and `p` is coprime to `deg g`, we conclude that `a` is
+  -- also a `p`-power, contradicting the hypothesis
+  have : p.Coprime (natDegree g) := hp.coprime_iff_not_dvd.mpr (fun e ↦ h (((natDegree_le_of_dvd hg'
+    (X_pow_sub_C_ne_zero hp.pos a)).trans_eq natDegree_X_pow_sub_C).antisymm (Nat.le_of_dvd
+      (natDegree_pos_iff_degree_pos.mpr <| Polynomial.degree_pos_of_irreducible hg) e)))
+  exact ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec
+
+theorem X_pow_sub_C_irreducible_iff_of_prime {p : ℕ} (hp : p.Prime) {a : K} :
+    Irreducible (X ^ p - C a) ↔ ∀ b, b ^ p ≠ a :=
+  ⟨(pow_ne_of_irreducible_X_pow_sub_C · dvd_rfl hp.ne_one), X_pow_sub_C_irreducible_of_prime hp⟩
+
+end Irreducible

Mathlib/FieldTheory/Perfect.lean

@@ -5,8 +5,8 @@ Authors: Oliver Nash
 -/
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.Algebra.CharP.Reduced
+import Mathlib.FieldTheory.KummerPolynomial
 import Mathlib.FieldTheory.Separable
-import Mathlib.FieldTheory.SplittingField.Construction
 
 /-!
 
@@ -203,35 +203,15 @@ instance ofFinite [Finite K] : PerfectField K := by
 variable [PerfectField K]
 
 /-- A perfect field of characteristic `p` (prime) is a perfect ring. -/
-instance toPerfectRing (p : ℕ) [ExpChar K p] : PerfectRing K p := by
+instance toPerfectRing (p : ℕ) [hp : ExpChar K p] : PerfectRing K p := by
   refine PerfectRing.ofSurjective _ _ fun y ↦ ?_
-  let f : K[X] := X ^ p - C y
-  let L := f.SplittingField
-  let ι := algebraMap K L
-  have hf_deg : f.degree ≠ 0 := by
-    rw [degree_X_pow_sub_C (expChar_pos K p) y, p.cast_ne_zero]; exact (expChar_pos K p).ne'
-  let a : L := f.rootOfSplits ι (SplittingField.splits f) hf_deg
-  have hfa : aeval a f = 0 := by rw [aeval_def, map_rootOfSplits _ (SplittingField.splits f) hf_deg]
-  have ha_pow : a ^ p = ι y := by rwa [map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hfa
-  let g : K[X] := minpoly K a
-  suffices (g.map ι).natDegree = 1 by
-    rw [g.natDegree_map, ← degree_eq_iff_natDegree_eq_of_pos Nat.one_pos] at this
-    obtain ⟨a' : K, ha' : ι a' = a⟩ := minpoly.mem_range_of_degree_eq_one K a this
-    refine ⟨a', NoZeroSMulDivisors.algebraMap_injective K L ?_⟩
-    rw [RingHom.map_frobenius, ha', frobenius_def, ha_pow]
-  have hg_dvd : g.map ι ∣ (X - C a) ^ p := by
-    convert Polynomial.map_dvd ι (minpoly.dvd K a hfa)
-    rw [sub_pow_expChar, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow]
-  have ha : IsIntegral K a := .of_finite K a
-  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]
-  have hg_sep : (g.map ι).Separable := (separable_of_irreducible <| minpoly.irreducible ha).map
-  rw [hg_pow] at hg_sep
-  refine (Separable.of_pow (not_isUnit_X_sub_C a) ?_ hg_sep).2
-  rw [g.natDegree_map ι, ← Nat.pos_iff_ne_zero, natDegree_pos_iff_degree_pos]
-  exact minpoly.degree_pos ha
+  rcases hp with _ | hp
+  · simp [frobenius]
+  rw [← not_forall_not]
+  apply mt (X_pow_sub_C_irreducible_of_prime hp)
+  apply mt separable_of_irreducible
+  simp [separable_def, isCoprime_zero_right, isUnit_iff_degree_eq_zero,
+    degree_X_pow_sub_C hp.pos, hp.ne_zero]
 
 theorem separable_iff_squarefree {g : K[X]} : g.Separable ↔ Squarefree g := by
   refine ⟨Separable.squarefree, fun sqf ↦ isCoprime_of_irreducible_dvd (sqf.ne_zero ·.1) ?_⟩