feat: port RingTheory.RootsOfUnity.Minpoly (#5119)

 - [x] depends on: #5076



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Mathlib.lean

@@ -2555,6 +2555,7 @@ import Mathlib.RingTheory.RingHomProperties
 import Mathlib.RingTheory.RingInvo
 import Mathlib.RingTheory.RootsOfUnity.Basic
 import Mathlib.RingTheory.RootsOfUnity.Complex
+import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.SimpleModule
 import Mathlib.RingTheory.Subring.Basic
 import Mathlib.RingTheory.Subring.Pointwise

Mathlib/RingTheory/RootsOfUnity/Minpoly.lean

@@ -0,0 +1,242 @@
+/-
+Copyright (c) 2020 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca, Johan Commelin
+
+! This file was ported from Lean 3 source module ring_theory.roots_of_unity.minpoly
+! leanprover-community/mathlib commit 7fdeecc0d03cd40f7a165e6cf00a4d2286db599f
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.RingTheory.RootsOfUnity.Basic
+import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
+
+/-!
+# Minimal polynomial of roots of unity
+
+We gather several results about minimal polynomial of root of unity.
+
+## Main results
+
+* `IsPrimitiveRoot.totient_le_degree_minpoly`: The degree of the minimal polynomial of a `n`-th
+  primitive root of unity is at least `totient n`.
+
+-/
+
+
+open minpoly Polynomial
+
+open scoped Polynomial
+
+namespace IsPrimitiveRoot
+
+section CommRing
+
+variable {n : ℕ} {K : Type _} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n)
+
+/-- `μ` is integral over `ℤ`. -/
+-- Porting note: `hpos` was in the `variable` line, with an `omit` in mathlib3 just after this
+-- declaration. For some reason, in Lean4, `hpos` gets included also in the declarations below,
+-- even if it is not used in the proof.
+theorem isIntegral (hpos : 0 < n) : IsIntegral ℤ μ := by
+  use X ^ n - 1
+  constructor
+  · exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm
+  · simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub,
+      sub_self]
+#align is_primitive_root.is_integral IsPrimitiveRoot.isIntegral
+
+section IsDomain
+
+variable [IsDomain K] [CharZero K]
+
+/-- The minimal polynomial of a root of unity `μ` divides `X ^ n - 1`. -/
+theorem minpoly_dvd_x_pow_sub_one : minpoly ℤ μ ∣ X ^ n - 1 := by
+  rcases n.eq_zero_or_pos with (rfl | h0)
+  · simp
+  apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)
+  simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow, eq_intCast, Int.cast_one,
+    aeval_one, AlgHom.map_sub, sub_self]
+set_option linter.uppercaseLean3 false in
+#align is_primitive_root.minpoly_dvd_X_pow_sub_one IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one
+
+/-- The reduction modulo `p` of the minimal polynomial of a root of unity `μ` is separable. -/
+theorem separable_minpoly_mod {p : ℕ} [Fact p.Prime] (hdiv : ¬p ∣ n) :
+    Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)) := by
+  have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 := by
+    simp [Polynomial.map_pow, map_X, Polynomial.map_one, Polynomial.map_sub]
+    convert  RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
+        (minpoly_dvd_x_pow_sub_one h)
+    simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]
+  refine' Separable.of_dvd (separable_X_pow_sub_C 1 _ one_ne_zero) hdvd
+  by_contra hzero
+  exact hdiv ((ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 hzero)
+#align is_primitive_root.separable_minpoly_mod IsPrimitiveRoot.separable_minpoly_mod
+
+/-- The reduction modulo `p` of the minimal polynomial of a root of unity `μ` is squarefree. -/
+theorem squarefree_minpoly_mod {p : ℕ} [Fact p.Prime] (hdiv : ¬p ∣ n) :
+    Squarefree (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)) :=
+  (separable_minpoly_mod h hdiv).squarefree
+#align is_primitive_root.squarefree_minpoly_mod IsPrimitiveRoot.squarefree_minpoly_mod
+
+/- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
+`μ ^ p`, where `p` is a natural number that does not divide `n`. Then `P` divides `expand ℤ p Q`. -/
+theorem minpoly_dvd_expand {p : ℕ} (hdiv : ¬p ∣ n) :
+    minpoly ℤ μ ∣ expand ℤ p (minpoly ℤ (μ ^ p)) := by
+  rcases n.eq_zero_or_pos with (rfl | hpos)
+  · simp_all
+  letI : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
+  refine' minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) _
+  · rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X,
+      eval_comp, eval_pow, eval_X, ← eval₂_eq_eval_map, ← aeval_def]
+    exact minpoly.aeval _ _
+#align is_primitive_root.minpoly_dvd_expand IsPrimitiveRoot.minpoly_dvd_expand
+
+/- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
+`μ ^ p`, where `p` is a prime that does not divide `n`. Then `P` divides `Q ^ p` modulo `p`. -/
+theorem minpoly_dvd_pow_mod {p : ℕ} [hprime : Fact p.Prime] (hdiv : ¬p ∣ n) :
+    map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣
+      map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) ^ p := by
+  set Q := minpoly ℤ (μ ^ p)
+  have hfrob :
+    map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (expand ℤ p Q) := by
+    rw [← ZMod.expand_card, map_expand]
+  rw [hfrob]
+  apply RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
+  exact minpoly_dvd_expand h hdiv
+#align is_primitive_root.minpoly_dvd_pow_mod IsPrimitiveRoot.minpoly_dvd_pow_mod
+
+/- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
+`μ ^ p`, where `p` is a prime that does not divide `n`. Then `P` divides `Q` modulo `p`. -/
+theorem minpoly_dvd_mod_p {p : ℕ} [hprime : Fact p.Prime] (hdiv : ¬p ∣ n) :
+    map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣
+      map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) :=
+  (UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree (squarefree_minpoly_mod h hdiv)
+        hprime.1.ne_zero).1
+    (minpoly_dvd_pow_mod h hdiv)
+#align is_primitive_root.minpoly_dvd_mod_p IsPrimitiveRoot.minpoly_dvd_mod_p
+
+/-- If `p` is a prime that does not divide `n`,
+then the minimal polynomials of a primitive `n`-th root of unity `μ`
+and of `μ ^ p` are the same. -/
+theorem minpoly_eq_pow {p : ℕ} [hprime : Fact p.Prime] (hdiv : ¬p ∣ n) :
+    minpoly ℤ μ = minpoly ℤ (μ ^ p) := by
+  classical
+  by_cases hn : n = 0
+  · simp_all
+  have hpos := Nat.pos_of_ne_zero hn
+  by_contra hdiff
+  set P := minpoly ℤ μ
+  set Q := minpoly ℤ (μ ^ p)
+  have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
+  have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
+  have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
+  have Qirr : Irreducible Q := minpoly.irreducible ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
+  have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
+  have prod : P * Q ∣ X ^ n - 1 := by
+    rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
+        (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
+      Polynomial.map_mul]
+    refine' IsCoprime.mul_dvd _ _ _
+    · have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
+      refine' (dvd_or_coprime _ _ (aux.1 Pirr)).resolve_left _
+      rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
+      intro hdiv
+      refine' hdiff (eq_of_monic_of_associated Pmonic Qmonic _)
+      exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
+    · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
+      exact minpoly_dvd_x_pow_sub_one h
+    · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
+      exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
+  replace prod := RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) prod
+  rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one,
+    Polynomial.map_pow, map_X] at prod
+  obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv
+  rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod
+  have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by
+    use R
+  replace habs :=
+    lt_of_lt_of_le (PartENat.coe_lt_coe.2 one_lt_two)
+      (multiplicity.le_multiplicity_of_pow_dvd (dvd_trans habs prod))
+  have hfree : Squarefree (X ^ n - 1 : (ZMod p)[X]) :=
+    (separable_X_pow_sub_C 1 (fun h => hdiv <| (ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 h)
+        one_ne_zero).squarefree
+  cases'
+    (multiplicity.squarefree_iff_multiplicity_le_one (X ^ n - 1)).1 hfree
+      (map (Int.castRingHom (ZMod p)) P) with
+    hle hunit
+  · rw [Nat.cast_one] at habs ; exact hle.not_lt habs
+  · replace hunit := degree_eq_zero_of_isUnit hunit
+    rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit
+    · exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit
+    simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne.def, not_false_iff,
+      one_ne_zero]
+#align is_primitive_root.minpoly_eq_pow IsPrimitiveRoot.minpoly_eq_pow
+
+/-- If `m : ℕ` is coprime with `n`,
+then the minimal polynomials of a primitive `n`-th root of unity `μ`
+and of `μ ^ m` are the same. -/
+theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.coprime m n) :
+    minpoly ℤ μ = minpoly ℤ (μ ^ m) := by
+  revert n hcop
+  refine' UniqueFactorizationMonoid.induction_on_prime m _ _ _
+  · intro h hn
+    congr
+    simpa [(Nat.coprime_zero_left _).mp hn] using h
+  · intro u hunit _ _
+    congr
+    simp [Nat.isUnit_iff.mp hunit]
+  · intro a p _ hprime
+    intro hind h hcop
+    rw [hind h (Nat.coprime.coprime_mul_left hcop)]; clear hind
+    replace hprime := hprime.nat_prime
+    have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.coprime.coprime_mul_right hcop)
+    haveI := Fact.mk hprime
+    rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.coprime.coprime_mul_left hcop)) hdiv]
+    congr 1
+    ring
+#align is_primitive_root.minpoly_eq_pow_coprime IsPrimitiveRoot.minpoly_eq_pow_coprime
+
+/-- If `m : ℕ` is coprime with `n`,
+then the minimal polynomial of a primitive `n`-th root of unity `μ`
+has `μ ^ m` as root. -/
+theorem pow_isRoot_minpoly {m : ℕ} (hcop : Nat.coprime m n) :
+    IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m) := by
+  simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]
+  exact minpoly.aeval ℤ (μ ^ m)
+#align is_primitive_root.pow_is_root_minpoly IsPrimitiveRoot.pow_isRoot_minpoly
+
+/-- `primitiveRoots n K` is a subset of the roots of the minimal polynomial of a primitive
+`n`-th root of unity `μ`. -/
+theorem is_roots_of_minpoly [DecidableEq K] :
+    primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset := by
+  by_cases hn : n = 0; · simp_all
+  have hpos := Nat.pos_of_ne_zero hn
+  intro x hx
+  obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h hpos).1 ((mem_primitiveRoots hpos).1 hx)
+  simp only [Multiset.mem_toFinset, mem_roots]
+  convert pow_isRoot_minpoly h hcop
+  rw [← mem_roots]
+  exact map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos
+#align is_primitive_root.is_roots_of_minpoly IsPrimitiveRoot.is_roots_of_minpoly
+
+/-- The degree of the minimal polynomial of `μ` is at least `totient n`. -/
+theorem totient_le_degree_minpoly : Nat.totient n ≤ (minpoly ℤ μ).natDegree := by
+  classical
+  let P : ℤ[X] := minpoly ℤ μ
+  -- minimal polynomial of `μ`
+  let P_K : K[X] := map (Int.castRingHom K) P
+  -- minimal polynomial of `μ` sent to `K[X]`
+  calc
+    n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
+    _ ≤ P_K.roots.toFinset.card := (Finset.card_le_of_subset (is_roots_of_minpoly h))
+    _ ≤ Multiset.card P_K.roots := (Multiset.toFinset_card_le _)
+    _ ≤ P_K.natDegree := (card_roots' _)
+    _ ≤ P.natDegree := natDegree_map_le _ _
+#align is_primitive_root.totient_le_degree_minpoly IsPrimitiveRoot.totient_le_degree_minpoly
+
+end IsDomain
+
+end CommRing
+
+end IsPrimitiveRoot