The local class formation

Let K be a nonarchimedean local field with separable closure Kˢ and absolute Galois group G_K. The formation TauCeti.ClassFieldTheory.unitsFormation K of the multiplicative group (Kˢ)ˣ, written additively, is a class formation (localClassFormation): its finite normal layers V ◁ U, the finite Galois extensions E'/E inside Kˢ, satisfy the axioms of TauCeti.ClassFieldTheory.ClassFormation with invariant map the invariant TauCeti.ClassFieldTheory.layerInv of the layer, that is, inflation into Br E = H²(U, (Kˢ)ˣ) followed by the local invariant of E. The axioms come from:

• Hilbert 90, for the vanishing of H¹ and the injectivity of inflation;
• the local invariant TauCeti.ClassFieldTheory.invMap and its restriction and corestriction squares, for the compatibility with restriction, inflation and conjugation;
• the local H² bound, through invMap being an isomorphism, for the range of the invariant.

On a layer V ◁ G_K over K itself, the invariant of the class formation is the local invariant of K on the Brauer class inflated by TauCeti.ClassFieldTheory.brInfl (localClassFormation_inv), so the invariant of the class formation and the invariant of the local Brauer group carry one normalization.

Main definitions

• TauCeti.ClassFieldTheory.localClassFormation K: the class formation of the units of a separable closure of a nonarchimedean local field.

Main results

• TauCeti.ClassFieldTheory.localClassFormation_inv: on a layer over K, the invariant of the class formation is invMap K ∘ brInfl.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §1.
• J.-P. Serre, Local Fields, Chapter XI, §§1–3.

Layers over K and the Brauer group

The local class formation

noncomputable def TauCeti.ClassFieldTheory.localClassFormation (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ClassFormation (unitsFormation K)

The local class formation: the formation of the units of a separable closure of a nonarchimedean local field K is a class formation, with the invariant layerInv of a layer as invariant map.

@[simp]

theorem TauCeti.ClassFieldTheory.localClassFormation_inv_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (unitsFormation K) 2)) : ((localClassFormation K).inv L) x = (layerInv K L) x

The invariant map of the local class formation is the invariant of a layer.

theorem TauCeti.ClassFieldTheory.localClassFormation_inv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (x : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation K) 2)) : ((localClassFormation K).inv (NormalLayer.ofOpenNormal V)) x = (invMap K) ((brInfl V) x)

The invariant of the local class formation is the local Brauer invariant: on the layer V ◁ G_K of an open normal subgroup, the invariant of a class is the local invariant invMap K of its inflation brInfl V into Br K.