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.

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 ℚ.

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.