Local degrees in the cyclotomic towers of prime-power level

Let K be a number field, ℓ a prime and v a finite place of K. Along the tower of cyclotomic extensions K(μ_{ℓ ^ r}) the local degrees at v become divisible by every power of ℓ: for each j, for all large r and every place w above v of an extension F/K of level ℓ ^ r, the power ℓ ^ j divides e(w ∣ v) f(w ∣ v) = [F_w : K_v] (IsCyclotomicExtension.eventually_pow_dvd_ramificationIdx_mul_inertiaDeg, IsCyclotomicExtension.eventually_pow_dvd_finrank_adicCompletion). The bound on r depends on v and j only, not on F.

The computation happens in the rational cyclotomic field ℚ(ζ) ⊆ F generated by a primitive ℓ ^ r-th root of unity ζ. Let p be the rational prime below v. If p = ℓ the prime ℓ is totally ramified in ℚ(ζ), with ramification index φ(ℓ ^ r); if p ≠ ℓ the residue degree of p in ℚ(ζ) is the order of p modulo ℓ ^ r, which is divisible by any given power of ℓ for large r (ZMod.eventually_pow_dvd_orderOf_natCast). Ramification indices and residue degrees are multiplicative in towers, so e(w ∣ p) f(w ∣ p) is a multiple of the corresponding product for ℚ(ζ) and equals [F_w : K_v] · e(v ∣ p) f(v ∣ p), where the last factor does not depend on r. An intermediate field E with [F : E] ≤ d inherits the divisibility, with j lowered by at most d: a prime of F contributes at most [F : E] to the fundamental identity of F/E.

This is the local input to the classical fact that a global Brauer class is split everywhere locally by a cyclic cyclotomic extension (Milne, Lemma VII.7.3). For ℓ odd the Galois group of K(μ_{ℓ ^ r})/K is cyclic; for ℓ = 2 the cyclic extension is a subfield of index at most two.

Main results

• IsCyclotomicExtension.eventually_pow_dvd_ramificationIdx_mul_inertiaDeg: ℓ ^ j divides e(w ∣ v) f(w ∣ v) at every prime w above v of every cyclotomic extension of level ℓ ^ r, for all large r.
• IsCyclotomicExtension.eventually_pow_dvd_finrank_adicCompletion: the same for the local degree [F_w : K_v] of the completions.
• IsCyclotomicExtension.eventually_pow_dvd_finrank_adicCompletion_of_finrank_le: the same for the local degrees of the intermediate fields E of F/K of bounded relative degree [F : E].

References

• J. S. Milne, Class Field Theory, Chapter VII, Lemma 7.3.
• J. Neukirch, Algebraic Number Theory, Chapter I, §10.

theorem IsCyclotomicExtension.eventually_pow_dvd_ramificationIdx_mul_inertiaDeg {K : Type u_1} [Field K] [NumberField K] {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (j : ℕ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ∀ᶠ (r : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [NumberField F] [inst_2 : Algebra K F] [IsCyclotomicExtension {ℓ ^ r} K F] (w : Ideal (NumberField.RingOfIntegers F)) [w.IsPrime] [w.LiesOver v.asIdeal], ℓ ^ j ∣ w.ramificationIdx (NumberField.RingOfIntegers K) * w.inertiaDeg (NumberField.RingOfIntegers K)

Ramification in the cyclotomic towers of prime-power level. Let v be a finite place of a number field K and ℓ a prime. For every j, the power ℓ ^ j divides the product e(w ∣ v) f(w ∣ v) of the ramification index and the residue degree at every prime w above v of every cyclotomic extension F/K of level ℓ ^ r, for all large r.

theorem IsCyclotomicExtension.eventually_pow_dvd_finrank_adicCompletion {K : Type u_1} [Field K] [NumberField K] {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (j : ℕ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ∀ᶠ (r : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [inst_1 : NumberField F] [inst_2 : Algebra K F] [IsCyclotomicExtension {ℓ ^ r} K F] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)) [inst_4 : w.asIdeal.LiesOver v.asIdeal], ℓ ^ j ∣ Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion F w)

Local degrees in the cyclotomic towers of prime-power level. Let v be a finite place of a number field K and ℓ a prime. For every j, the power ℓ ^ j divides the local degree [F_w : K_v] at every place w above v of every cyclotomic extension F/K of level ℓ ^ r, for all large r.

theorem IsCyclotomicExtension.eventually_pow_dvd_finrank_adicCompletion_of_finrank_le {K : Type u_1} [Field K] [NumberField K] {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (j d : ℕ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ∀ᶠ (r : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [inst_1 : NumberField F] [inst_2 : Algebra K F] [IsCyclotomicExtension {ℓ ^ r} K F] (E : IntermediateField K F), Module.finrank (↥E) F ≤ d → ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ↥E)) [inst_4 : w.asIdeal.LiesOver v.asIdeal], ℓ ^ j ∣ Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion (↥E) w)

Local degrees of subextensions of bounded index in the cyclotomic towers. Let v be a finite place of a number field K, ℓ a prime and d a natural number. For every j, the power ℓ ^ j divides the local degree [E_w : K_v] at every place w above v of every intermediate field E of relative degree [F : E] ≤ d in a cyclotomic extension F/K of level ℓ ^ r, for all large r.