Brauer invariants at archimedean completions

For an infinite place w, infiniteInvMap w is the invariant of the cohomological Brauer group of Mathlib's completion w.Completion. At a real place it sends the unique nonzero class to 1/2 in ℚ/ℤ; at a complex place the Brauer group vanishes. Its image is consequently the two-torsion subgroup at a real place and zero at a complex place.

These maps provide the archimedean terms in sums of local Brauer invariants. The real value is intrinsic: it depends only on whether the class vanishes, not on an identification of separable closures used to transport the real Brauer-group calculation. infiniteInvMap_eq_realInv_comp makes this independence explicit for every additive identification with the real Brauer group.

References

• J.-P. Serre, Local Fields, Chapter XIII, §1.
• J. S. Milne, Class Field Theory, Chapter VIII, §4.

noncomputable def TauCeti.ClassFieldTheory.infiniteInvMap {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) : Br w.Completion →+ AddCircle 1

The archimedean Brauer invariant on the canonical completion: the normalized real invariant at a real place, and the zero map at a complex place.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteInvMap_of_isReal {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : infiniteInvMap w = realInv.comp (brCongr (NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hw)).toAddMonoidHom

At a real place the archimedean invariant is the real invariant transported through Mathlib's identification of the completion with ℝ.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteInvMap_of_isComplex {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) : infiniteInvMap w = 0

At a complex place the archimedean invariant is the zero homomorphism.

theorem TauCeti.ClassFieldTheory.brCompletion_eq_zero_of_isComplex {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) (x : Br w.Completion) : x = 0

The Brauer group of a complex completion is trivial.

theorem TauCeti.ClassFieldTheory.infiniteInvMap_apply_eq_ite {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (x : Br w.Completion) : (infiniteInvMap w) x = if x = 0 then 0 else ↑(1 / 2)

The invariant is zero on the zero class and 1/2 on every nonzero class: at a real place by the real Brauer group, at a complex place because the Brauer group is trivial.

theorem TauCeti.ClassFieldTheory.infiniteInvMap_eq_realInv_comp {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (e : Br w.Completion ≃+ Br ℝ) : infiniteInvMap w = realInv.comp e.toAddMonoidHom

Every additive identification with the real Brauer group gives the same normalized invariant (at a complex place there is no such identification, since the Brauer group is trivial). In particular, changing the lift of a field isomorphism to separable closures does not change the invariant.

theorem TauCeti.ClassFieldTheory.infiniteInvMap_eq_zero_of_isComplex {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) (x : Br w.Completion) : (infiniteInvMap w) x = 0

The invariant at a complex place always vanishes.

theorem TauCeti.ClassFieldTheory.range_infiniteInvMap_of_isReal {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : Set.range ⇑(infiniteInvMap w) = ↑(AddSubgroup.torsionBy (AddCircle 1) 2)

At a real place the image of the invariant is precisely the two-torsion of ℚ/ℤ.

theorem TauCeti.ClassFieldTheory.range_infiniteInvMap_of_isComplex {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) : Set.range ⇑(infiniteInvMap w) = {0}

At a complex place the image of the invariant is the singleton zero.

theorem TauCeti.ClassFieldTheory.infiniteInvMap_injective {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) : Function.Injective ⇑(infiniteInvMap w)

Every archimedean invariant is injective, including at a complex place where its domain is trivial.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteInvMap_eq_zero_iff {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (x : Br w.Completion) : (infiniteInvMap w) x = 0 ↔ x = 0

An archimedean invariant vanishes exactly when its Brauer class vanishes.

theorem TauCeti.ClassFieldTheory.exists_infiniteInvMap_eq_half_of_isReal {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) : ∃ (x : Br w.Completion), (infiniteInvMap w) x = ↑(1 / 2)

At every real place there is a Brauer class with invariant 1/2.