The local invariants of a global Brauer class

Let K be a number field. For every place of K this file defines the local invariant of a cohomological Brauer class x ∈ Br K = H²(G_K, (Kˢ)ˣ), the first ingredients of the global Brauer sequence

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

The localization map at a place is base change TauCeti.ClassFieldTheory.brBaseChange to the completion, that is, restriction to the decomposition group, and the local invariant is the invariant of the local Brauer class:

• at a finite place v, finiteInvAt K v x = inv_{K_v} (x ⊗ K_v), with the invariant TauCeti.ClassFieldTheory.invMap of the nonarchimedean local field v.adicCompletion K, normalized by arithmetic Frobenius;
• at an infinite place w, infiniteInvAt K w x is the archimedean invariant TauCeti.ClassFieldTheory.infiniteInvMap w of x ⊗ K_w, which is 0 at a complex place and 0 or 1/2 at a real place.

Both are additive in x, and each vanishes exactly when the localization of x does, since the local invariant maps are injective. The invariants at the infinite places make sense, and are defined, for every field with its infinite places.

Main definitions

• TauCeti.ClassFieldTheory.finiteInvAt K v: the local invariant Br K → ℚ/ℤ at a finite place.
• TauCeti.ClassFieldTheory.infiniteInvAt K w: the local invariant Br K → ℚ/ℤ at an infinite place.

Main results

• TauCeti.ClassFieldTheory.finiteInvAt_eq_zero_iff, TauCeti.ClassFieldTheory.infiniteInvAt_eq_zero_iff: a local invariant vanishes exactly when the localization does.
• TauCeti.ClassFieldTheory.infiniteInvAt_eq_zero_of_isComplex: the invariants at complex places vanish.
• TauCeti.ClassFieldTheory.infiniteInvAt_mem_torsionBy_two: the archimedean invariants are killed by 2.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (8.1.17).
• J. S. Milne, Class Field Theory, Chapter VIII, §4.

Infinite places

noncomputable def TauCeti.ClassFieldTheory.infiniteInvAt (K : Type) [Field K] (w : NumberField.InfinitePlace K) : Br K →+ AddCircle 1

The local invariant at an infinite place w of a field K: the archimedean invariant of the localization Br K → Br K_w.

theorem TauCeti.ClassFieldTheory.infiniteInvAt_apply (K : Type) [Field K] (w : NumberField.InfinitePlace K) (x : Br K) : (infiniteInvAt K w) x = (infiniteInvMap w) ((brBaseChange K w.Completion) x)

The local invariant at an infinite place is the archimedean invariant of the localization.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteInvAt_eq_zero_iff (K : Type) [Field K] (w : NumberField.InfinitePlace K) (x : Br K) : (infiniteInvAt K w) x = 0 ↔ (brBaseChange K w.Completion) x = 0

The local invariant at an infinite place vanishes exactly when the localization of the class vanishes.

theorem TauCeti.ClassFieldTheory.infiniteInvAt_eq_zero_of_isComplex (K : Type) [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) (x : Br K) : (infiniteInvAt K w) x = 0

The local invariant at a complex place vanishes.

theorem TauCeti.ClassFieldTheory.infiniteInvAt_mem_torsionBy_two (K : Type) [Field K] (w : NumberField.InfinitePlace K) (x : Br K) : (infiniteInvAt K w) x ∈ AddSubgroup.torsionBy (AddCircle 1) 2

The local invariants at the infinite places are killed by 2: they lie in {0, 1/2}.

Finite places

noncomputable def TauCeti.ClassFieldTheory.finiteInvAt (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Br K →+ AddCircle 1

The local invariant at a finite place v of a number field K: the invariant of the nonarchimedean local field K_v of the localization Br K → Br K_v, x ↦ inv_{K_v} (x ⊗ K_v).

theorem TauCeti.ClassFieldTheory.finiteInvAt_apply (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : Br K) : (finiteInvAt K v) x = (invMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((brBaseChange K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x)

The local invariant at a finite place is the invariant of the localization.

@[simp]

theorem TauCeti.ClassFieldTheory.finiteInvAt_eq_zero_iff (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : Br K) : (finiteInvAt K v) x = 0 ↔ (brBaseChange K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x = 0

The local invariant at a finite place vanishes exactly when the localization of the class vanishes.