Surjectivity of the sum of local Brauer invariants

The sum of local invariants in the global Brauer sequence

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

has an additive section supported at any chosen finite place. The local invariant is an additive equivalence at that place, so every element of ℚ/ℤ is the invariant of a family supported there. In particular, sumLocalInv is surjective.

The same calculation shows that a family of local Brauer classes can be adjusted at one finite place to have any prescribed total invariant, and that the adjustment is unique. This is a statement about local families; it does not assert that a family of total invariant zero is the localization of a global Brauer class.

The section uses DFinsupp.singleAddHom and the inverse of TauCeti.ClassFieldTheory.invMap, the local invariant normalized by arithmetic Frobenius. The single-place API takes an explicit decidable-equality instance, as DFinsupp.single does, so its equations rewrite families constructed with any such instance. Consumers may supply it with classical; the surjectivity theorem itself needs no decidable-equality instance.

Main definitions

• TauCeti.ClassFieldTheory.sumLocalInvSection: an additive section supported at a chosen finite place.

Main statements

• TauCeti.ClassFieldTheory.sumLocalInvSection_apply: the section's single-supported family.
• TauCeti.ClassFieldTheory.sumLocalInv_sumLocalInvSection: the section is a right inverse.
• TauCeti.ClassFieldTheory.sumLocalInv_surjective: the sum of local invariants is surjective.
• TauCeti.ClassFieldTheory.sumLocalInv_add_single_eq_iff: the unique adjustment at a finite place giving a prescribed total invariant.

References

• J. S. Milne, Class Field Theory, Chapter VIII, §4, Theorem 4.2.

noncomputable def TauCeti.ClassFieldTheory.sumLocalInvSection (K : Type) [Field K] [NumberField K] [DecidableEq (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : AddCircle 1 →+ (Π₀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Br (IsDedekindDomain.HeightOneSpectrum.adicCompletion K w)) × ((w : NumberField.InfinitePlace K) → Br w.Completion)

An additive section of the sum of local invariants, supported at the chosen finite place v. Its class at v has invariant the given element of ℚ/ℤ.

@[simp]

theorem TauCeti.ClassFieldTheory.sumLocalInvSection_apply (K : Type) [Field K] [NumberField K] [DecidableEq (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (r : AddCircle 1) : (sumLocalInvSection K v) r = (DFinsupp.single v ((invMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).symm r), 0)

The section is the family supported at v with the prescribed local invariant.

theorem TauCeti.ClassFieldTheory.sumLocalInv_sumLocalInvSection (K : Type) [Field K] [NumberField K] [DecidableEq (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (r : AddCircle 1) : (sumLocalInv K) ((sumLocalInvSection K v) r) = r

Taking the sum of local invariants after the section recovers the prescribed invariant.

theorem TauCeti.ClassFieldTheory.sumLocalInv_surjective (K : Type) [Field K] [NumberField K] : Function.Surjective ⇑(sumLocalInv K)

The sum of local Brauer invariants is surjective for every number field.

theorem TauCeti.ClassFieldTheory.sumLocalInv_add_single_eq_iff (K : Type) [Field K] [NumberField K] [DecidableEq (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (y : (Π₀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Br (IsDedekindDomain.HeightOneSpectrum.adicCompletion K w)) × ((w : NumberField.InfinitePlace K) → Br w.Completion)) (x : Br (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (r : AddCircle 1) : (sumLocalInv K) (y + (DFinsupp.single v x, 0)) = r ↔ x = (invMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).symm (r - (sumLocalInv K) y)

A prescribed total invariant determines the unique adjustment of a local family at a chosen finite place.