The ramified primes of a cyclotomic extension of a number field

Let M / K be an m-th cyclotomic extension with K a number field. The level m lies in the different ideal of 𝓞 M over 𝓞 K — equivalently, that different divides (m) — so ramification in M / K is confined to the primes above m. Read through absolute discriminants, along the factorisation |discr M| = 𝔑 𝔡(𝓞 M / 𝓞 K) * |discr K| ^ [M : K], the same bound says that a rational prime dividing discr M divides discr K or divides m: the extension ramifies only below or at the level.

Neither statement constrains m against K. In that they differ from the degree identity [M : K] = φ m of TauCeti.NumberTheory.NumberField.Cyclotomic.Finrank, which needs m coprime to discr K and fails outright when K already contains a primitive m-th root of unity.

Over ℚ the ramification at the level is explicit: in ℚ(ζ_{p k}) with p ∤ k the prime p has ramification index p - 1, so ζ_p - 1 is a uniformizer at every prime above p.

Main results

• IsCyclotomicExtension.natCast_mem_differentIdeal: the level m lies in the different ideal of 𝓞 M over 𝓞 K.
• IsCyclotomicExtension.isUnramifiedAt_of_natCast_notMem: primes above an ideal not containing the level are unramified.
• IsCyclotomicExtension.prime_dvd_natAbs_discr_or_dvd_of_dvd_natAbs_discr: a prime dividing discr M divides discr K or divides m — the extension ramifies only below or at the level.
• IsCyclotomicExtension.Rat.intValuation_sub_one_eq_exp_neg_one: in ℚ(ζ_{p k}) with p ∤ k, a primitive p-th root of unity ζ has v(ζ - 1) = 1 at every prime above p.

Implementation notes

natCast_mem_differentIdeal reads as a membership rather than as a divisibility of Ideal.span {(m : 𝓞 M)}; Ideal.span_singleton_le_iff_mem gives the divisibility form where that is the one wanted.

natCast_mem_differentIdeal and prime_dvd_natAbs_discr_or_dvd_of_dvd_natAbs_discr ask M to be a number field alongside K, because their statements mention differentIdeal (𝓞 K) (𝓞 M) (which needs IsDedekindDomain (𝓞 M)) and NumberField.discr M. That is no restriction, since a cyclotomic extension of a number field is one: IsCyclotomicExtension.numberField {m} K M, which isUnramifiedAt_of_natCast_notMem, whose statement needs neither, uses to supply the instance itself.

theorem IsCyclotomicExtension.natCast_mem_differentIdeal (K : Type u_1) (M : Type u_2) [Field K] [NumberField K] [Field M] [NumberField M] [Algebra K M] (m : ℕ) [IsCyclotomicExtension {m} K M] : ↑m ∈ differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers M)

The level lies in the different ideal. For M / K an m-th cyclotomic extension of number fields, m belongs to the different ideal of 𝓞 M over 𝓞 K; equivalently that different divides (m), so only primes dividing m can ramify in M / K.

theorem IsCyclotomicExtension.isUnramifiedAt_of_natCast_notMem {K : Type u_1} [Field K] [NumberField K] (F : Type u_2) [Field F] [Algebra K F] (m : ℕ) [IsCyclotomicExtension {m} K F] {p : Ideal (NumberField.RingOfIntegers K)} (hm : ↑m ∉ p) (Q : Ideal (NumberField.RingOfIntegers F)) [Q.IsPrime] [Q.LiesOver p] : Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q

In a cyclotomic extension of level m, every prime above an ideal not containing m is unramified.

theorem IsCyclotomicExtension.prime_dvd_natAbs_discr_or_dvd_of_dvd_natAbs_discr (K : Type u_1) (M : Type u_2) [Field K] [NumberField K] [Field M] [NumberField M] [Algebra K M] (m : ℕ) [IsCyclotomicExtension {m} K M] {p : ℕ} (hp : Nat.Prime p) (hpM : p ∣ (NumberField.discr M).natAbs) : p ∣ (NumberField.discr K).natAbs ∨ p ∣ m

A prime ramifying in a cyclotomic extension either ramifies below or divides the level. For M / K an m-th cyclotomic extension of number fields, a prime dividing discr M divides discr K or divides m.

theorem IsCyclotomicExtension.Rat.intValuation_sub_one_eq_exp_neg_one {L : Type u_1} [Field L] [NumberField L] {p k : ℕ} [Fact (Nat.Prime p)] [IsCyclotomicExtension {p * k} ℚ L] (hpk : ¬p ∣ k) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver (Ideal.span {↑p})] {ζ : NumberField.RingOfIntegers L} (hζ : IsPrimitiveRoot ζ p) : w.intValuation (ζ - 1) = WithZero.exp (-1)

ζ - 1 is a uniformizer above p. Let L be the p k-th cyclotomic field with p prime and p ∤ k. At every prime w of L above p, a primitive p-th root of unity ζ satisfies v_w(ζ - 1) = 1, because p has ramification index p - 1 in L.