The local invariant of the Brauer group

Let K be a nonarchimedean local field with separable closure Kˢ. This file proves that every class of the Brauer group Br K = H²(G_K, (Kˢ)ˣ) is split by an unramified extension of K, and constructs the local invariant

inv_K : Br K ≃+ ℚ/ℤ,

normalized by arithmetic Frobenius: on a class inflated from an unramified layer E/K inside Kˢ it is the invariant TauCeti.ClassFieldTheory.unramifiedInv K E of the layer.

Let E/K be a finite Galois extension inside Kˢ of degree n, and let Kₙ be the unramified extension of degree n inside Kˢ. The classes of Br K split by E and by Kₙ are the same. Indeed, let x ∈ H²(Gal(Kₙ/K), Kₙˣ) and let M = E Kₙ. The extension M/E is unramified, and the restriction of x to H²(Gal(M/E), Mˣ) has invariant [E : K] · inv_K(x) = n · inv_K(x) (TauCeti.ClassFieldTheory.unramifiedInv_map_baseChange), which vanishes since inv_K(x) has order dividing n. So the inflation of x to Br K is split by E (TauCeti.ClassFieldTheory.relBrInfl_mem_range_relBrInfl_iff). The classes split by Kₙ thus form a subgroup of order n (TauCeti.ClassFieldTheory.natCard_H2_unramified) of the classes split by E, which have order dividing n (TauCeti.natCard_H2_units_dvd_finrank), so the two groups agree. Since every Brauer class is split by some finite Galois extension (TauCeti.ClassFieldTheory.exists_relBrInfl_eq), the unramified Brauer group TauCeti.ClassFieldTheory.unramifiedBr K is all of Br K, and its invariant TauCeti.ClassFieldTheory.unramifiedBrInv K is defined on the whole Brauer group.

Let L/K be a finite extension of nonarchimedean local fields, embedded in Kˢ. Restriction TauCeti.ClassFieldTheory.brRes K L σ multiplies the invariant by [L : K]. Indeed, a class inflated from the unramified extension K_f/K of degree f restricts to the class inflated along the base change H²(Gal(K_f/K), K_fˣ) → H²(Gal(L_f/L), L_fˣ), where L_f/L is the unramified extension of degree f, which contains the image of K_f under the identification Kˢ ≃ Lˢ (TauCeti.unramifiedExtension_le_restrictScalars_unramifiedExtension, TauCeti.ClassFieldTheory.brBaseChange_eq_brRes, TauCeti.ClassFieldTheory.brBaseChange_relBrInfl), and this base change multiplies the unramified invariant by [L : K] (TauCeti.ClassFieldTheory.unramifiedInv_map_baseChange). Since multiplication by [L : K] is surjective on ℚ/ℤ, restriction is surjective, and corestriction TauCeti.ClassFieldTheory.brCor K L σ preserves the invariant because brCor ∘ brRes = [L : K] (TauCeti.ClassFieldTheory.brCor_brRes).

Main definitions

• TauCeti.ClassFieldTheory.invMap K: the local invariant Br K ≃+ ℚ/ℤ.

Main results

• TauCeti.ClassFieldTheory.range_relBrInfl_eq_range_relBrInfl_unramifiedExtension: a Brauer class is split by a finite Galois extension of degree n exactly when it is split by the unramified extension of degree n.
• TauCeti.ClassFieldTheory.unramifiedBr_eq_top: every Brauer class is split by an unramified extension.
• TauCeti.ClassFieldTheory.invMap_eq_unramifiedBrInv: the local invariant is the invariant of the unramified Brauer group.
• TauCeti.ClassFieldTheory.invMap_relBrInfl: on a class inflated from an unramified layer, the invariant is the invariant unramifiedInv of the layer.
• TauCeti.ClassFieldTheory.invMap_relBrInfl_unramified: the same, for an unramified extension embedded in Kˢ by an arbitrary embedding.
• TauCeti.ClassFieldTheory.range_invMap_comp_relBrInfl: the invariants of the classes split by a finite normal extension L/K embedded in Kˢ by σ are the elements of ℚ/ℤ killed by [L : K].
• TauCeti.ClassFieldTheory.invMap_brRes: the restriction square inv_L (brRes x) = [L : K] • inv_K x.
• TauCeti.ClassFieldTheory.brRes_surjective: restriction of Brauer classes is surjective.
• TauCeti.ClassFieldTheory.invMap_brCor: the corestriction square inv_K (brCor y) = inv_L y.
• TauCeti.ClassFieldTheory.brCor_bijective: corestriction of Brauer classes is bijective.
• TauCeti.ClassFieldTheory.brBaseChange_eq_zero_of_dvd_finrank: a finite extension of degree divisible by n splits every n-torsion Brauer class.
• TauCeti.ClassFieldTheory.brBaseChange_eq_zero_of_isPrimitiveRoot: a root of unity of order q^n - 1 splits every n-torsion Brauer class of a nonarchimedean local field.

References

• J. S. Milne, Class Field Theory, Chapter VII, Proposition 7.2 and Lemma 7.3.
• J.-P. Serre, Local Fields, Chapter XIII, §3.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI (Serre, Local Class Field Theory), §1.

theorem TauCeti.ClassFieldTheory.range_relBrInfl_eq_range_relBrInfl_unramifiedExtension (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [Normal K ↥E] : (relBrInfl K (↥E) E.val).range = (relBrInfl K (↥(unramifiedExtension K (SeparableClosure K) (Module.finrank K ↥E))) (unramifiedExtension K (SeparableClosure K) (Module.finrank K ↥E)).val).range

A Brauer class is split by a finite Galois extension of degree n exactly when it is split by the unramified extension of degree n. For E/K finite normal inside Kˢ, the classes of Br K inflated from H²(Gal(E/K), Eˣ) are those inflated from H²(Gal(Kₙ/K), Kₙˣ), where Kₙ is the unramified extension of degree n = [E : K] inside Kˢ.

@[simp]

theorem TauCeti.ClassFieldTheory.unramifiedBr_eq_top (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : unramifiedBr K = ⊤

Every Brauer class of a nonarchimedean local field is split by an unramified extension.

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

The local invariant inv_K : Br K ≃+ ℚ/ℤ of a nonarchimedean local field K, normalized by arithmetic Frobenius: on the classes inflated from an unramified extension E/K inside Kˢ it is the invariant TauCeti.ClassFieldTheory.unramifiedInv K E of the layer (invMap_relBrInfl).

theorem TauCeti.ClassFieldTheory.invMap_eq_unramifiedBrInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Br K) (hx : x ∈ unramifiedBr K) : (invMap K) x = (unramifiedBrInv K) ⟨x, hx⟩

The local invariant of a Brauer class is its invariant in the unramified Brauer group.

@[simp]

theorem TauCeti.ClassFieldTheory.invMap_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)) : (invMap K) ((relBrInfl K (↥E) E.val) y) = (unramifiedInv K ↥E) y

The normalization of the local 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ˣ).

theorem TauCeti.ClassFieldTheory.invMap_relBrInfl_unramified (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (ι : L →ₐ[K] SeparableClosure K) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)) : (invMap K) ((relBrInfl K L ι) y) = (unramifiedInv K L) y

The local invariant of a class inflated from a finite unramified Galois extension L/K, embedded in Kˢ by an arbitrary ι, is its invariant unramifiedInv K L in the layer H²(Gal(L/K), Lˣ).

Restriction and corestriction

@[simp]

theorem TauCeti.ClassFieldTheory.invMap_brRes (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (σ : L →ₐ[K] SeparableClosure K) (x : Br K) : (invMap L) ((brRes K L σ) x) = Module.finrank K L • (invMap K) x

The restriction square of the local invariant: restriction of Brauer classes along a finite extension L/K of nonarchimedean local fields multiplies the invariant by the degree, inv_L (res x) = [L : K] · inv_K x.

theorem TauCeti.ClassFieldTheory.range_invMap_comp_relBrInfl (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] [Normal K L] : Set.range (⇑(invMap K) ∘ ⇑(relBrInfl K L σ)) = ↑(AddSubgroup.torsionBy (AddCircle 1) ↑(Module.finrank K L))

The degree-n piece of the Brauer group. For a finite normal extension L/K of nonarchimedean local fields embedded in Kˢ by σ, the invariants of the classes split by L are exactly the elements of ℚ/ℤ killed by [L : K].

theorem TauCeti.ClassFieldTheory.brRes_surjective (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (σ : L →ₐ[K] SeparableClosure K) : Function.Surjective ⇑(brRes K L σ)

Restriction of Brauer classes along a finite extension of nonarchimedean local fields is surjective, since multiplication by [L : K] is surjective on ℚ/ℤ.

@[simp]

theorem TauCeti.ClassFieldTheory.invMap_brCor (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (y : Br L) : (invMap K) ((brCor K L σ) y) = (invMap L) y

The corestriction square of the local invariant: corestriction of Brauer classes along a finite extension L/K of nonarchimedean local fields preserves the invariant, inv_K (cor y) = inv_L y.

theorem TauCeti.ClassFieldTheory.brCor_bijective (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : Function.Bijective ⇑(brCor K L σ)

Corestriction of Brauer classes along a finite extension of nonarchimedean local fields is bijective, since it preserves the invariant.

theorem TauCeti.ClassFieldTheory.brBaseChange_eq_zero_of_dvd_finrank (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L] {n : ℕ} (hn : n ∣ Module.finrank K L) (x : Br K) (hx : n • x = 0) : (brBaseChange K L) x = 0

A finite extension of degree divisible by n splits every n-torsion Brauer class of a nonarchimedean local field, since base change multiplies the invariant by the degree.

theorem TauCeti.ClassFieldTheory.brBaseChange_eq_zero_of_isPrimitiveRoot {F L : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [Field L] [Algebra F L] {n : ℕ} (hn : n ≠ 0) {ζ : L} (hζ : IsPrimitiveRoot ζ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation F).integer) ^ n - 1)) (x : Br F) (hx : n • x = 0) : (brBaseChange F L) x = 0

Adjoining a primitive (q^n - 1)-st root of unity splits every n-torsion Brauer class of a nonarchimedean local field with residue cardinality q. The extension need not be finite or carry a valuation.