feat(PerfectRing): roots of Polynomial.expand (#9311)

Inspired by #9271

Prove the main theorem `rootMultiplicity_expand` and derive corollaries about `Polynomial.roots`. Refactor `rootsExpand(Pow)EquivRoots` using the new lemmas.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: acmepjz <acme_pjz@hotmail.com>

Mathlib/Data/Polynomial/Eval.lean

@@ -1115,6 +1115,9 @@ theorem iterate_comp_eval :
   iterate_comp_eval₂ _
 #align polynomial.iterate_comp_eval Polynomial.iterate_comp_eval
 
+lemma isRoot_comp {R} [CommSemiring R] {p q : R[X]} {r : R} :
+    (p.comp q).IsRoot r ↔ p.IsRoot (q.eval r) := by simp_rw [IsRoot, eval_comp]
+
 /-- `comp p`, regarded as a ring homomorphism from `R[X]` to itself. -/
 def compRingHom : R[X] → R[X] →+* R[X] :=
   eval₂RingHom C

Mathlib/Data/Polynomial/Expand.lean

@@ -43,6 +43,8 @@ theorem coe_expand : (expand R p : R[X] → R[X]) = eval₂ C (X ^ p) :=
 
 variable {R}
 
+theorem expand_eq_comp_X_pow {f : R[X]} : expand R p f = f.comp (X ^ p) := rfl
+
 theorem expand_eq_sum {f : R[X]} : expand R p f = f.sum fun e a => C a * (X ^ p) ^ e := by
   simp [expand, eval₂]
 #align polynomial.expand_eq_sum Polynomial.expand_eq_sum
@@ -275,6 +277,25 @@ end ExpChar
 
 end CommSemiring
 
+section rootMultiplicity
+
+variable {R : Type u} [CommRing R] {p n : ℕ} [ExpChar R p] {f : R[X]} {r : R}
+
+theorem rootMultiplicity_expand_pow :
+    (expand R (p ^ n) f).rootMultiplicity r = p ^ n * f.rootMultiplicity (r ^ p ^ n) := by
+  obtain rfl | h0 := eq_or_ne f 0; · simp
+  obtain ⟨g, hg, ndvd⟩ := f.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h0 (r ^ p ^ n)
+  rw [dvd_iff_isRoot, ← eval_X (x := r), ← eval_pow, ← isRoot_comp, ← expand_eq_comp_X_pow] at ndvd
+  conv_lhs => rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
+    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
+      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]
+
+theorem rootMultiplicity_expand :
+    (expand R p f).rootMultiplicity r = p * f.rootMultiplicity (r ^ p) := by
+  rw [← pow_one p, rootMultiplicity_expand_pow]
+
+end rootMultiplicity
+
 section IsDomain
 
 variable (R : Type u) [CommRing R] [IsDomain R]

Mathlib/FieldTheory/Perfect.lean

@@ -89,6 +89,14 @@ noncomputable def iterateFrobeniusEquiv : R ≃+* R :=
 @[simp]
 theorem coe_iterateFrobeniusEquiv : ⇑(iterateFrobeniusEquiv R p n) = iterateFrobenius R p n := rfl
 
+theorem iterateFrobeniusEquiv_eq_pow : iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n :=
+  DFunLike.ext' <| show _ = ⇑(RingAut.toPerm _ _) by
+    rw [map_pow, Equiv.Perm.coe_pow]; exact (pow_iterate p n).symm
+
+theorem iterateFrobeniusEquiv_symm :
+    (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n := by
+  rw [iterateFrobeniusEquiv_eq_pow]; exact (inv_pow _ _).symm
+
 @[simp]
 theorem frobeniusEquiv_symm_apply_frobenius (x : R) :
     (frobeniusEquiv R p).symm (frobenius R p x) = x :=
@@ -131,43 +139,6 @@ instance instPerfectRingProd (S : Type*) [CommSemiring S] [ExpChar S p] [Perfect
     PerfectRing (R × S) p where
   bijective_frobenius := (bijective_frobenius R p).Prod_map (bijective_frobenius S p)
 
-namespace Polynomial
-
-open scoped Classical
-
-variable {R : Type*} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] [PerfectRing R p] (f : R[X])
-
-/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
-a bijection from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
-It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`. -/
-noncomputable def rootsExpandEquivRoots : (expand R p f).roots.toFinset ≃ f.roots.toFinset :=
-  ((frobeniusEquiv R p).image _).trans <| Equiv.Set.ofEq <| show _ '' (setOf _) = setOf _ by
-    ext r; obtain ⟨r, rfl⟩ := surjective_frobenius R p r
-    simp [expand_eq_zero (expChar_pos R p), (frobenius_inj R p).eq_iff, ← frobenius_def]
-
-@[simp]
-theorem rootsExpandEquivRoots_apply (x) : (rootsExpandEquivRoots p f x : R) = x ^ p := rfl
-
-/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
-a bijection from the set of roots of `Polynomial.expand R (p ^ n) f` to the set of roots of `f`.
-It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowEquivRoots_apply`. -/
-noncomputable def rootsExpandPowEquivRoots :
-    (n : ℕ) → (expand R (p ^ n) f).roots.toFinset ≃ f.roots.toFinset
-  | 0 => Equiv.Set.ofEq <| by rw [pow_zero, expand_one]
-  | n + 1 => (Equiv.Set.ofEq <| by rw [pow_succ, ← expand_expand]).trans
-    (rootsExpandEquivRoots p (expand R (p ^ n) f)) |>.trans (rootsExpandPowEquivRoots n)
-
-@[simp]
-theorem rootsExpandPowEquivRoots_apply (n : ℕ) (x) :
-    (rootsExpandPowEquivRoots p f n x : R) = x ^ p ^ n := by
-  induction' n with n ih
-  · simp only [pow_zero, pow_one]
-    rfl
-  simp_rw [rootsExpandPowEquivRoots, Equiv.trans_apply, ih, pow_succ, pow_mul]
-  rfl
-
-end Polynomial
-
 end PerfectRing
 
 /-- A perfect field.
@@ -250,3 +221,123 @@ theorem Algebra.IsAlgebraic.perfectField {K L : Type*} [Field K] [Field L] [Alge
     [PerfectField K] (halg : Algebra.IsAlgebraic K L) : PerfectField L := ⟨fun {f} hf ↦ by
   obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral halg.isIntegral
   exact (PerfectField.separable_of_irreducible hi).map |>.of_dvd h⟩
+
+namespace Polynomial
+
+variable {R : Type*} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : R[X])
+
+open Multiset
+
+theorem roots_expand_pow_map_iterateFrobenius_le :
+    (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) ≤ p ^ n • f.roots := by
+  classical
+  refine le_iff_count.2 fun r ↦ ?_
+  by_cases h : ∃ s, r = s ^ p ^ n
+  · obtain ⟨s, rfl⟩ := h
+    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
+      count_eq_card_filter_eq]
+    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
+  convert Nat.zero_le _
+  simp_rw [count_map, card_eq_zero]
+  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩
+
+theorem roots_expand_map_frobenius_le :
+    (expand R p f).roots.map (frobenius R p) ≤ p • f.roots := by
+  rw [← iterateFrobenius_one]
+  convert ← roots_expand_pow_map_iterateFrobenius_le p 1 f <;> apply pow_one
+
+theorem roots_expand_pow_image_iterateFrobenius_subset [DecidableEq R] :
+    (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) ⊆ f.roots.toFinset := by
+  rw [Finset.image_toFinset, ← (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne',
+    toFinset_subset]
+  exact subset_of_le (roots_expand_pow_map_iterateFrobenius_le p n f)
+
+theorem roots_expand_image_frobenius_subset [DecidableEq R] :
+    (expand R p f).roots.toFinset.image (frobenius R p) ⊆ f.roots.toFinset := by
+  rw [← iterateFrobenius_one]
+  convert ← roots_expand_pow_image_iterateFrobenius_subset p 1 f
+  apply pow_one
+
+variable {p n f}
+
+variable [PerfectRing R p]
+
+theorem roots_expand_pow :
+    (expand R (p ^ n) f).roots = p ^ n • f.roots.map (iterateFrobeniusEquiv R p n).symm := by
+  classical
+  refine ext' fun r ↦ ?_
+  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
+    count_eq_card_filter_eq]; congr; ext
+  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm
+
+theorem roots_expand : (expand R p f).roots = p • f.roots.map (frobeniusEquiv R p).symm := by
+  conv_lhs => rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]
+
+theorem roots_expand_pow_map_iterateFrobenius :
+    (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) = p ^ n • f.roots := by
+  simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
+    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']
+
+theorem roots_expand_map_frobenius : (expand R p f).roots.map (frobenius R p) = p • f.roots := by
+  simp [roots_expand, Multiset.map_nsmul]
+
+theorem roots_expand_image_iterateFrobenius [DecidableEq R] :
+    (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) = f.roots.toFinset := by
+  rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
+    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']
+
+theorem roots_expand_image_frobenius [DecidableEq R] :
+    (expand R p f).roots.toFinset.image (frobenius R p) = f.roots.toFinset := by
+  rw [Finset.image_toFinset, roots_expand_map_frobenius,
+      (roots f).toFinset_nsmul _ (expChar_pos R p).ne']
+
+variable (p n f) [DecidableEq R]
+
+/-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is
+a map from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
+It's given by `x ↦ x ^ p`, see `rootsExpandToRoots_apply`. -/
+noncomputable def rootsExpandToRoots : (expand R p f).roots.toFinset ↪ f.roots.toFinset where
+  toFun x := ⟨x ^ p, roots_expand_image_frobenius_subset p f (Finset.mem_image_of_mem _ x.2)⟩
+  inj' _ _ h := Subtype.ext (frobenius_inj R p <| Subtype.ext_iff.1 h)
+
+@[simp]
+theorem rootsExpandToRoots_apply (x) : (rootsExpandToRoots p f x : R) = x ^ p := rfl
+
+open scoped Classical in
+/-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is
+a map from the set of roots of `Polynomial.expand R (p ^ n) f` to the set of roots of `f`.
+It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowToRoots_apply`. -/
+noncomputable def rootsExpandPowToRoots :
+    (expand R (p ^ n) f).roots.toFinset ↪ f.roots.toFinset where
+  toFun x := ⟨x ^ p ^ n,
+    roots_expand_pow_image_iterateFrobenius_subset p n f (Finset.mem_image_of_mem _ x.2)⟩
+  inj' _ _ h := Subtype.ext (iterateFrobenius_inj R p n <| Subtype.ext_iff.1 h)
+
+@[simp]
+theorem rootsExpandPowToRoots_apply (x) : (rootsExpandPowToRoots p n f x : R) = x ^ p ^ n := rfl
+
+/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
+a bijection from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
+It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`. -/
+noncomputable def rootsExpandEquivRoots : (expand R p f).roots.toFinset ≃ f.roots.toFinset :=
+  ((frobeniusEquiv R p).image _).trans <| .Set.ofEq <| show _ '' (setOf _) = setOf _ by
+    classical simp_rw [← roots_expand_image_frobenius (p := p) (f := f), Finset.mem_val,
+      Finset.setOf_mem, Finset.coe_image]; rfl
+
+@[simp]
+theorem rootsExpandEquivRoots_apply (x) : (rootsExpandEquivRoots p f x : R) = x ^ p := rfl
+
+/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
+a bijection from the set of roots of `Polynomial.expand R (p ^ n) f` to the set of roots of `f`.
+It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowEquivRoots_apply`. -/
+noncomputable def rootsExpandPowEquivRoots (n : ℕ) :
+    (expand R (p ^ n) f).roots.toFinset ≃ f.roots.toFinset :=
+  ((iterateFrobeniusEquiv R p n).image _).trans <| .Set.ofEq <| show _ '' (setOf _) = setOf _ by
+    classical simp_rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n),
+      Finset.mem_val, Finset.setOf_mem, Finset.coe_image]; rfl
+
+@[simp]
+theorem rootsExpandPowEquivRoots_apply (n : ℕ) (x) :
+    (rootsExpandPowEquivRoots p f n x : R) = x ^ p ^ n := rfl
+
+end Polynomial