The sum of the local invariants of a Brauer class

Let K be a number field. The global Brauer sequence

0 → Br K → ⨁_v Br K_v → ℚ/ℤ → 0

has zero composite Br K → ℚ/ℤ exactly when the local invariants of every global Brauer class sum to zero; this is the inclusion of the image of Br K in the kernel of the sum, one half of exactness in the middle. This file proves that sum formula for every class of Br K (sumLocalInv_brLocalization_eq_zero) from the Hasse principle, injectivity of Br E → ⨁_w Br E_w, over the finite extensions E of K. The Hasse principle (brLocalization_injective) follows from the vanishing of idele-class H¹ (TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_h1_globalFormation), which comes with the second fundamental inequality (TauCeti.ClassFieldTheory.subsingleton_h1_globalFormation).

The argument is Milne's Lemma 8.6. A Brauer class is torsion, so it is a sum of classes killed by powers of primes, and the sum of the local invariants is additive. Let x be killed by a power of a prime ℓ. For r large, the cyclotomic field K(μ_{ℓ^r}) contains a cyclic extension E of K that kills every localization of x (TauCeti.ClassFieldTheory.eventually_exists_isCyclic_brLocalization_eq_zero). By the Hasse principle over E, the class x itself dies in E, so it is inflated from H²(Gal(E/K), Eˣ) (TauCeti.ClassFieldTheory.mem_range_relBrInfl_iff_brBaseChange_eq_zero). For classes split by a cyclic subextension of a cyclotomic extension, the sum formula comes from the product formula for the local Artin symbols on cyclotomic extensions (TauCeti.ClassFieldTheory.sumLocalInv_brLocalization_relBrInfl_eq_zero_of_le_adjoin_nth_roots).

Main results

• TauCeti.ClassFieldTheory.brLocalization_injective: the Hasse principle: a Brauer class of K with trivial localizations at all places is zero.
• TauCeti.ClassFieldTheory.sumLocalInv_brLocalization_eq_zero: the local invariants of every Brauer class of K sum to zero.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemma 8.6 and Theorem 8.1, and Chapter VIII, Theorem 4.2.

theorem TauCeti.ClassFieldTheory.brLocalization_injective (K : Type) [Field K] [NumberField K] : Function.Injective ⇑(brLocalization K)

The Hasse principle for the Brauer group (Albert–Brauer–Hasse–Noether). A Brauer class of the number field K whose localizations at all places vanish is zero: Br K → ⨁_v Br K_v is injective.

@[simp]

theorem TauCeti.ClassFieldTheory.sumLocalInv_brLocalization_eq_zero (K : Type) [Field K] [NumberField K] (x : Br K) : (sumLocalInv K) ((brLocalization K) x) = 0

The sum formula. The local invariants of every Brauer class of the number field K sum to zero.