Irreducibility of the cyclotomic polynomial from the degree of a cyclotomic extension

Mathlib proves [L : K] = φ n for an n-th cyclotomic extension L / K once Φ_n is known to be irreducible over K (IsCyclotomicExtension.finrank). This file records the converse: the degree of L / K is always at most φ n, and as soon as it is at least φ n the polynomial Φ_n is irreducible over K. That converse and Mathlib's forward direction give the equivalence IsCyclotomicExtension.irreducible_cyclotomic_iff_finrank_eq_totient.

Main results

• IsCyclotomicExtension.finrank_le_totient: [L : K] ≤ φ n.
• IsCyclotomicExtension.irreducible_cyclotomic_of_totient_le_finrank: if φ n ≤ [L : K] then Φ_n is irreducible over K.
• IsCyclotomicExtension.irreducible_cyclotomic_iff_finrank_eq_totient: Φ_n is irreducible over K if and only if [L : K] = φ n.
• irreducible_cyclotomic_of_coprime_finrank: irreducibility is preserved by a finite base change whose degree is coprime to φ n.
• irreducible_cyclotomic_prime_pow_ratPadic: every p-power cyclotomic polynomial is irreducible over ℚ_p.

References

This is the degree bookkeeping of Milne, Algebraic Number Theory, proof of Proposition 6.2, and of Sharifi, Algebraic Number Theory, proof of Lemma 3.1.13, where the base field is ℚ. For local cyclotomic irreducibility, see Serre, Local Fields, Chapter IV, §4; the proof uses Mathlib's cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt.

theorem IsCyclotomicExtension.finrank_le_totient {n : ℕ} [NeZero n] (K : Type u_1) [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] : Module.finrank K L ≤ n.totient

The degree of a cyclotomic extension is at most φ n.

The bound is unconditional: nothing is assumed about cyclotomic n K. That is what separates it from Mathlib's IsCyclotomicExtension.finrank, which gives the sharper [L : K] = φ n but only under Irreducible (cyclotomic n K). Reach for this one when that irreducibility is unknown, or is itself what is being proved.

Source: Milne, Algebraic Number Theory, proof of Prop. 6.2 ("we know [ℚ[ζ] : ℚ] ≤ φ(p^r)"); Sharifi, Algebraic Number Theory, proof of Lemma 3.1.13 ("[ℚ(µ_{p^r}) : ℚ] ≤ deg Φ_{p^r}").

theorem IsCyclotomicExtension.irreducible_cyclotomic_of_totient_le_finrank {n : ℕ} [NeZero n] (K : Type u_1) [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : n.totient ≤ Module.finrank K L) : Irreducible (Polynomial.cyclotomic n K)

A cyclotomic extension of full degree has irreducible cyclotomic polynomial. This is the converse of Mathlib's IsCyclotomicExtension.finrank, and with it gives the equivalence irreducible_cyclotomic_iff_finrank_eq_totient.

Source: Milne, Algebraic Number Theory, proof of Prop. 6.2 ("(3.34) implies [ℚ[ζ] : ℚ] ≥ φ(p^r). This proves (a)"); Sharifi, proof of Lemma 3.1.13 ("which forces [ℚ(µ_{p^r}) : ℚ] = p^{r−1}(p − 1)").

theorem IsCyclotomicExtension.irreducible_cyclotomic_iff_finrank_eq_totient {n : ℕ} [NeZero n] (K : Type u_1) [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] : Irreducible (Polynomial.cyclotomic n K) ↔ Module.finrank K L = n.totient

Φ_n is irreducible over K exactly when the cyclotomic extension has degree φ n. The forward direction is Mathlib's IsCyclotomicExtension.finrank; the converse is irreducible_cyclotomic_of_totient_le_finrank.

Source: as for the two lemmas it combines.

theorem TauCeti.irreducible_cyclotomic_prime_pow_ratPadic (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Irreducible (Polynomial.cyclotomic (p ^ n) ℚ_[p])

The p^n-th cyclotomic polynomial is irreducible over ℚ_p. In particular, the local cyclotomic extension generated by a primitive p^n-th root has degree φ(p^n).

theorem TauCeti.irreducible_cyclotomic_of_coprime_finrank {n : ℕ} {F : Type u_1} [Field F] {K : Type u_2} [Field K] [Algebra F K] [FiniteDimensional F K] (hirr : Irreducible (Polynomial.cyclotomic n F)) (hcop : n.totient.Coprime (Module.finrank F K)) : Irreducible (Polynomial.cyclotomic n K)

Irreducibility of Φ_n is preserved by a finite base change of degree coprime to φ(n). This is useful for transporting cyclotomic irreducibility through extensions whose degrees have no common factor with the cyclotomic degree. No assumption on the characteristic is needed: the proof only uses that Φ_n is monic of degree φ(n).

Source: the linear-disjointness theory in Lang, Algebra, revised third edition, Chapter VIII, §3.