Cyclotomic extensions that split a Brauer class locally

A class of the Brauer group of a number field becomes trivial at every completion after extension to a suitable cyclotomic field. At a finite place with residue cardinality q, adjoining a primitive (q^n - 1)-st root of unity gives an unramified subextension of degree n. Thus an n-torsion local Brauer class vanishes there. There are only finitely many nontrivial finite localizations, so one cyclotomic modulus handles them all. A factor of four in the modulus makes every infinite place complex.

A class killed by a power ℓ ^ k of a prime ℓ is already split locally by the cyclotomic field of level ℓ ^ r for all large r: the local degrees of these fields at a given place become divisible by ℓ ^ k (IsCyclotomicExtension.eventually_pow_dvd_finrank_adicCompletion), and a local extension of degree divisible by ℓ ^ k splits every ℓ ^ k-torsion local class. For ℓ odd this field is a cyclic extension, which is what the computation of the sum of the local invariants through the local Artin symbols of a character requires. For ℓ = 2 it is not cyclic once r ≥ 3, but it contains a totally complex subfield, cyclic over K, of index at most two (TauCeti.NumberField.exists_isTotallyComplex_isCyclic_subextension_prime_pow). Its local degrees above a given place are those of the cyclotomic field divided by at most two, so they too become divisible by ℓ ^ k (IsCyclotomicExtension.eventually_pow_dvd_finrank_adicCompletion_of_finrank_le), and it still splits the class locally. Hence, for every prime ℓ, every cyclotomic extension of level ℓ ^ r with r large contains a cyclic extension of K that kills all localizations of a class killed by a power of ℓ (eventually_exists_isCyclic_brLocalization_eq_zero).

The conclusion is local splitting, not global splitting: deducing the latter requires injectivity of Brauer localization. The local statement supplies the cyclotomic splitting input to the sum-of-local-invariants argument without assuming a global reciprocity law.

Main results

• TauCeti.ClassFieldTheory.brLocalization_brBaseChange_eq_zero_of_forall: an extension without real places kills all localizations of a Brauer class once it kills them above its support.
• TauCeti.ClassFieldTheory.exists_cyclotomicField_brLocalization_eq_zero: one cyclotomic extension kills all localizations of a global Brauer class.
• TauCeti.ClassFieldTheory.eventually_cyclotomicField_brLocalization_eq_zero: the cyclotomic fields of level ℓ ^ r, for all large r, kill all localizations of a Brauer class killed by a power of ℓ.
• TauCeti.ClassFieldTheory.eventually_exists_isCyclic_brLocalization_eq_zero: so do cyclic subextensions of the cyclotomic extensions of level ℓ ^ r, for all large r.

References

• J. S. Milne, Class Field Theory, Chapter VII, Proposition 7.2 and Lemma 7.3.

theorem TauCeti.ClassFieldTheory.brLocalization_brBaseChange_eq_zero_of_forall (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [NumberField.IsTotallyComplex L] (x : Br K) (h : ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∈ brauerSupport K x → (brBaseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K (IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) ((brBaseChange K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K (IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w))) x) = 0) : (brLocalization L) ((brBaseChange K L) x) = 0

An extension L of a number field K without real places kills all localizations of a Brauer class x of K as soon as, at every place w of L above a place v in the support of x, the local class of x at v dies in the extension L_w / K_v.

theorem TauCeti.ClassFieldTheory.exists_cyclotomicField_brLocalization_eq_zero (K : Type) [Field K] [NumberField K] (x : Br K) : ∃ (m : ℕ), m ≠ 0 ∧ 4 ∣ m ∧ (brLocalization (CyclotomicField m K)) ((brBaseChange K (CyclotomicField m K)) x) = 0

A cyclotomic extension of a number field kills all localizations of a given Brauer class. The modulus is divisible by four, so the resulting field has no real places. This theorem makes no assertion that the global base-changed class itself vanishes.

theorem TauCeti.ClassFieldTheory.eventually_cyclotomicField_brLocalization_eq_zero (K : Type) [Field K] [NumberField K] {ℓ : ℕ} (hℓ : Nat.Prime ℓ) {k : ℕ} (x : Br K) (hx : ℓ ^ k • x = 0) : ∀ᶠ (r : ℕ) in Filter.atTop, (brLocalization (CyclotomicField (ℓ ^ r) K)) ((brBaseChange K (CyclotomicField (ℓ ^ r) K)) x) = 0

The cyclotomic tower of level ℓ ^ r splits ℓ-primary Brauer classes locally. A Brauer class of a number field killed by a power of a prime ℓ has trivial localizations at every place after extension to the cyclotomic field of level ℓ ^ r, for all large r. For ℓ odd this extension is cyclic (IsCyclotomicExtension.isCyclic_aut, with ZMod.isCyclic_units_of_prime_pow). This theorem makes no assertion that the global base-changed class itself vanishes.

theorem TauCeti.ClassFieldTheory.eventually_exists_isCyclic_brLocalization_eq_zero (K : Type) [Field K] [NumberField K] {ℓ : ℕ} (hℓ : Nat.Prime ℓ) {k : ℕ} (x : Br K) (hx : ℓ ^ k • x = 0) : ∀ᶠ (r : ℕ) in Filter.atTop, ∀ (F : Type) [inst : Field F] [inst_1 : NumberField F] [inst_2 : Algebra K F] [IsCyclotomicExtension {ℓ ^ r} K F], ∃ (E : IntermediateField K F), IsGalois K ↥E ∧ IsCyclic Gal(↥E/K) ∧ (brLocalization ↥E) ((brBaseChange K ↥E) x) = 0

Cyclic cyclotomic extensions split ℓ-primary Brauer classes locally. Let x be a Brauer class of a number field K killed by a power of a prime ℓ. For all large r, every cyclotomic extension F/K of level ℓ ^ r contains an intermediate field E, Galois with cyclic Galois group over K, after extension to which all localizations of x vanish. This theorem makes no assertion that the global base-changed class itself vanishes.