English
There exists a polynomial P ∈ ℤ[X] such that map (Int.castRingHom K) P = cyclotomic' n K and deg P equals deg cyclotomic' n K and P is monic.
Русский
Существует полином P ∈ ℤ[X], такой что отображение в K через целочисленное отображение даёт cyclotomic' n K, и deg P совпадает с deg cyclotomic' n K, и P моничен.
LaTeX
$$$\exists P \in \mathbb{Z}[X],\ map(\operatorname{Int.castRingHom}K)P = \operatorname{cyclotomic}'(n,K) \land P.\deg = (\operatorname{cyclotomic}'(n,K)).\deg \land P.Monic$$$
Lean4
/-- If there is a primitive `n`-th root of unity in `K`, then `cyclotomic' n K` comes from a
monic polynomial with integer coefficients. -/
theorem int_coeff_of_cyclotomic' {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
∃ P : ℤ[X], map (Int.castRingHom K) P = cyclotomic' n K ∧ P.degree = (cyclotomic' n K).degree ∧ P.Monic :=
by
refine lifts_and_degree_eq_and_monic ?_ (cyclotomic'.monic n K)
induction n using Nat.strong_induction_on generalizing ζ with
| _ k ihk
rcases k.eq_zero_or_pos with (rfl | hpos)
· use 1
simp only [cyclotomic'_zero, coe_mapRingHom, Polynomial.map_one]
let B : K[X] := ∏ i ∈ Nat.properDivisors k, cyclotomic' i K
have Bmo : B.Monic := by
apply monic_prod_of_monic
intro i _
exact cyclotomic'.monic i K
have Bint : B ∈ lifts (Int.castRingHom K) :=
by
refine Subsemiring.prod_mem (lifts (Int.castRingHom K)) ?_
intro x hx
have xsmall := (Nat.mem_properDivisors.1 hx).2
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1
rw [mul_comm] at hd
exact ihk x xsmall (h.pow hpos hd)
replace Bint := lifts_and_degree_eq_and_monic Bint Bmo
obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint
let Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
have huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ (0 : K[X]).degree < B.degree :=
by
constructor
·
rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← Nat.cons_self_properDivisors hpos.ne',
Finset.prod_cons]
· simpa only [degree_zero, bot_lt_iff_ne_bot, Ne, degree_eq_bot] using Bmo.ne_zero
replace huniq := div_modByMonic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq
simp only [lifts, RingHom.mem_rangeS]
use Q₁
rw [coe_mapRingHom, map_divByMonic (Int.castRingHom K) hB₁mo, hB₁, ← huniq.1]
simp
