From e7a73bf30c29611b0ebbb0c169de94977fbc459c Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sat, 10 Feb 2024 09:09:01 +0000 Subject: [PATCH] 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 Co-authored-by: acmepjz --- Mathlib/Data/Polynomial/Eval.lean | 3 + Mathlib/Data/Polynomial/Expand.lean | 21 ++++ Mathlib/FieldTheory/Perfect.lean | 165 +++++++++++++++++++++------- 3 files changed, 152 insertions(+), 37 deletions(-) diff --git a/Mathlib/Data/Polynomial/Eval.lean b/Mathlib/Data/Polynomial/Eval.lean index 5dd01d3a479a7..95c9309a91d79 100644 --- a/Mathlib/Data/Polynomial/Eval.lean +++ b/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 diff --git a/Mathlib/Data/Polynomial/Expand.lean b/Mathlib/Data/Polynomial/Expand.lean index fef1a1f3981a4..21d69ebd29b2a 100644 --- a/Mathlib/Data/Polynomial/Expand.lean +++ b/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] diff --git a/Mathlib/FieldTheory/Perfect.lean b/Mathlib/FieldTheory/Perfect.lean index e9c69c90f04dd..0b68a3fbb3656 100644 --- a/Mathlib/FieldTheory/Perfect.lean +++ b/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