The invariant of the unramified Brauer group

Let K be a nonarchimedean local field with separable closure Kˢ. For every f ≥ 1, the unramified extension K_f = TauCeti.unramifiedExtension K Kˢ f of degree f carries the local invariant TauCeti.ClassFieldTheory.unramifiedInv K K_f : H²(Gal(K_f/K), K_fˣ) → ℚ/ℤ, normalized by arithmetic Frobenius, injective with image the subgroup of order f. This file glues these invariants along the inflations relBrInfl K K_f : H²(Gal(K_f/K), K_fˣ) → Br K into the invariant of the unramified Brauer group

Br(Kⁿʳ/K) = ⋃_f relBrInfl K K_f (H²(Gal(K_f/K), K_fˣ)) ≤ Br K,

the subgroup of the Brauer classes split by an unramified extension.

The images of the layers form a directed family: for f ∣ g, K_f ⊆ K_g, and inflation H²(Gal(K_f/K), K_fˣ) → H²(Gal(K_g/K), K_gˣ) commutes with the inflations into Br K (TauCeti.ClassFieldTheory.relBrInfl_map) and preserves the invariant (TauCeti.ClassFieldTheory.unramifiedInv_map). Since each relBrInfl is injective, a class inflated from two layers has the same invariant in both, which defines the invariant on Br(Kⁿʳ/K). It is injective because each layer invariant is, and surjective onto ℚ/ℤ because every element of ℚ/ℤ has finite order f, and the invariant of K_f has image the elements of order dividing f.

Every Brauer class is in fact split by an unramified extension (TauCeti.ClassFieldTheory.unramifiedBr_eq_top), so this is the invariant of the full Brauer group (TauCeti.ClassFieldTheory.invMap).

Main definitions

• TauCeti.ClassFieldTheory.unramifiedBr K: the unramified Brauer group Br(Kⁿʳ/K) ≤ Br K.
• TauCeti.ClassFieldTheory.unramifiedBrInv K: its invariant Br(Kⁿʳ/K) ≃+ ℚ/ℤ.

Main results

• TauCeti.ClassFieldTheory.mem_unramifiedBr_iff: a Brauer class is unramified exactly when it is inflated from the unramified extension of some degree.
• TauCeti.ClassFieldTheory.relBrInfl_mem_unramifiedBr: a class inflated from any unramified extension of K inside Kˢ is unramified.
• TauCeti.ClassFieldTheory.unramifiedBrInv_relBrInfl: on such a class, the invariant is the invariant unramifiedInv of the layer.

Implementation notes

An unramified extension E of K inside Kˢ carries no preferred topology or valuative relation, but any two compatible with those of K agree (TauCeti.algebraicExtensionValuativeRel_eq, TauCeti.algebraicExtensionNormedFieldTopology_eq), so unramifiedInv K E does not depend on the choice. The statements are made for an arbitrary compatible structure, and the construction uses that of TauCeti.algebraicExtensionValuativeRel.

References

• J.-P. Serre, Local Fields, Chapter XII, §1.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI (Serre, Local Class Field Theory), §1.

noncomputable def TauCeti.ClassFieldTheory.unramifiedBr (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : AddSubgroup (Br K)

The unramified Brauer group Br(Kⁿʳ/K): the subgroup of Br K of the classes inflated from H²(Gal(L/K), Lˣ) for the unramified extensions L of K of every degree f ≥ 1 inside Kˢ (TauCeti.unramifiedExtension).

theorem TauCeti.ClassFieldTheory.mem_unramifiedBr_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {x : Br K} : x ∈ unramifiedBr K ↔ ∃ (f : ℕ+) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥(unramifiedExtension K (SeparableClosure K) ↑f)/K) (↥(unramifiedExtension K (SeparableClosure K) ↑f))ˣ) 2)), (relBrInfl K (↥(unramifiedExtension K (SeparableClosure K) ↑f)) (unramifiedExtension K (SeparableClosure K) ↑f).val) y = x

x ∈ Br K lies in the unramified Brauer group exactly when it is inflated from the unramified extension of some degree f ≥ 1.

noncomputable def TauCeti.ClassFieldTheory.unramifiedBrInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ↥(unramifiedBr K) ≃+ AddCircle 1

The invariant of the unramified Brauer group inv : Br(Kⁿʳ/K) ≃ ℚ/ℤ, normalized by arithmetic Frobenius: on the classes inflated from an unramified extension L/K inside Kˢ it is the invariant TauCeti.ClassFieldTheory.unramifiedInv K L of the layer (unramifiedBrInv_relBrInfl).

theorem TauCeti.ClassFieldTheory.relBrInfl_mem_unramifiedBr {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [Normal K ↥E] [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension K ↥E] [IsUnramified K ↥E] (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥E/K) (↥E)ˣ) 2)) : (relBrInfl K (↥E) E.val) y ∈ unramifiedBr K

A class inflated from an unramified extension E of K inside Kˢ lies in the unramified Brauer group.

@[simp]

theorem TauCeti.ClassFieldTheory.unramifiedBrInv_relBrInfl {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [IsGalois K ↥E] [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension K ↥E] [IsUnramified K ↥E] (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥E/K) (↥E)ˣ) 2)) : (unramifiedBrInv K) ⟨(relBrInfl K (↥E) E.val) y, ⋯⟩ = (unramifiedInv K ↥E) y

The normalization of the unramified invariant: a class inflated from an unramified extension E of K inside Kˢ has invariant its invariant unramifiedInv K E in the layer H²(Gal(E/K), Eˣ).