The degree of a cyclotomic extension of a number field

Mathlib computes the degree of an m-th cyclotomic extension either over ℚ (IsCyclotomicExtension.Rat.finrank) or over a base for which the m-th cyclotomic polynomial is already known to be irreducible (IsCyclotomicExtension.finrank). Neither is directly usable over a general number field K, where irreducibility of Φ_m over K is exactly what has to be established.

This file supplies the arithmetic criterion: if m is coprime to the discriminant of K, then

[M : K] = φ m for M / K an m-th cyclotomic extension with K a number field.

The mechanism is linear disjointness rather than a direct irreducibility argument. Inside M, the two subfields ℚ(ζ) and (the image of) K have coprime discriminants, so Mathlib's NumberField.linearDisjoint_of_isGalois_isCoprime_discr makes them linearly disjoint; their compositum is M, so the degree of M over K equals the degree of ℚ(ζ) over ℚ, which is φ m. Coprimality of the discriminants is where the hypothesis is spent, via the divisibility input below.

Main results

• IsCyclotomicExtension.Rat.prime_dvd_of_dvd_natAbs_discr: a prime dividing the discriminant of an m-th cyclotomic field divides m. This is the divisibility input that turns coprimality to m into coprimality of discriminants.
• IsCyclotomicExtension.finrank_eq_totient: the degree identity [M : K] = φ m.

Implementation notes

The hypothesis is ((NumberField.discr K).natAbs).Coprime m, a statement about the base field. It is the condition an arithmetic caller can actually arrange — e.g. by choosing m to be a prime unramified in K — whereas the resulting intersection or irreducibility conditions would have to be re-derived from it at each use.

Only the base K carries a NumberField hypothesis. M is finite over K by IsCyclotomicExtension.finiteDimensional, hence a number field on its own, so demanding [NumberField M] of the caller would be an avoidable hypothesis. The degree itself comes from linear disjointness of ℚ(ζ) and the image of K inside M, whose compositum is M.

Adapted from the Birkbeck–Brasca Chebotarev density project.

theorem IsCyclotomicExtension.Rat.prime_dvd_of_dvd_natAbs_discr (E : Type u_1) [Field E] [NumberField E] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} ℚ E] {p : ℕ} (hp : Nat.Prime p) (hpd : p ∣ (NumberField.discr E).natAbs) : p ∣ m

A prime dividing the discriminant of an m-th cyclotomic extension of ℚ divides m.

theorem IsCyclotomicExtension.finrank_eq_totient (K : Type u_1) (M : Type u_2) [Field K] [NumberField K] [Field M] [Algebra K M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K M] (hcop : (NumberField.discr K).natAbs.Coprime m) : Module.finrank K M = m.totient

The cyclotomic degree over a number field base. If M / K is an m-th cyclotomic extension with K a number field and m coprime to discr K, then [M : K] = φ m.

Coprimality to discr K stands in for irreducibility of Φ_m over K, and is the hypothesis an arithmetic caller can arrange directly. Only the base K need be a number field.