English
If p is a prime not dividing n, then the minimal polynomials of μ and μ^p over ℤ are equal.
Русский
Если p — простое число, не делящее n, то минимальные полиномы μ и μ^p над ℤ равны.
LaTeX
$$$\minpoly_{\mathbb{Z}}(\mu) = \minpoly_{\mathbb{Z}}(\mu^{p})$$$
Lean4
/-- 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_isCoprime _ _ (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 := _root_.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 (Nat.cast_lt.2 one_lt_two) (le_emultiplicity_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.natCast_eq_zero_iff n p).1 h) one_ne_zero).squarefree
rcases (squarefree_iff_emultiplicity_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_gt 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, not_false_iff, one_ne_zero]
