The 2-torsion of the Brauer group as H²(G_K, 𝔽₂)

Let K be a field in which 2 is invertible. This file identifies the 2-torsion subgroup Br(K)[2] of the Brauer group with continuous cohomology of the absolute Galois group with trivial 𝔽₂ coefficients,

brauer2EquivH2 K : Additive Br(K)[2] ≃+ H²_cont(G_K, 𝔽₂),

which in classical notation is Br(K)[2] ≃ H²(G_K, μ₂).

The identification is assembled from two maps already available. The comparison TauCeti.brauerCohomologyEquiv K : Additive (Br K) ≃+ H²_cont(G_K, (Kˢ)ˣ) identifies the whole Brauer group with cohomology with multiplicative coefficients, and the Kummer map TauCeti.h2MuToUnits K : H²_cont(G_K, 𝔽₂) → H²_cont(G_K, (Kˢ)ˣ) is injective with image the 2-torsion (TauCeti.h2MuToUnits_injective, TauCeti.h2MuToUnits_range). An additive equivalence carries 2-torsion onto 2-torsion, so the two 2-torsion subgroups match.

The identification has no normalization of its own: it is the unique additive equivalence making the square

Br(K)[2]  ─────── brauer2EquivH2 ──────→  H²_cont(G_K, 𝔽₂)
   │                                            │
   │ inclusion                                  │ h2MuToUnits
   ↓                                            ↓
 Br(K)  ─────── brauerCohomologyEquiv ───→  H²_cont(G_K, (Kˢ)ˣ)

commute (TauCeti.brauer2EquivH2_h2MuToUnits, TauCeti.brauer2EquivH2_unique), so every statement about it is a statement about TauCeti.brauerCohomologyEquiv read through the injective map TauCeti.h2MuToUnits.

Main definitions

• TauCeti.BrauerGroup.twoTorsion K: the subgroup Br(K)[2] of classes whose square is trivial.
• TauCeti.brauer2EquivH2 K: the identification Additive Br(K)[2] ≃+ H²_cont(G_K, 𝔽₂).

Main results

• TauCeti.brauer2EquivH2_h2MuToUnits: the square above commutes.
• TauCeti.brauer2EquivH2_unique: the commuting square determines the identification.
• TauCeti.brauer2EquivH2_symm_apply: the inverse identification sends a class y to the Brauer class corresponding to h2MuToUnits K y under the comparison.

References

• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §4.4.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, (6.2.1) and the exact sequence following it.

def TauCeti.BrauerGroup.twoTorsion (K : Type u) [Field K] : Subgroup (BrauerGroup K)

The 2-torsion of the Brauer group, Br(K)[2]: the classes whose square is trivial, as the kernel of squaring.

Equations

• TauCeti.BrauerGroup.twoTorsion K = (powMonoidHom 2).ker

@[simp]

theorem TauCeti.BrauerGroup.mem_twoTorsion {K : Type u} [Field K] {x : BrauerGroup K} : x ∈ twoTorsion K ↔ x ^ 2 = 1

A Brauer class is 2-torsion exactly when its square is trivial.

noncomputable def TauCeti.brauer2EquivH2 (K : Type) [Field K] [Invertible 2] : Additive ↥(BrauerGroup.twoTorsion K) ≃+ ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat

The 2-torsion of the Brauer group is H²(G_K, 𝔽₂). The identification Br(K)[2] ≃ H²_cont(G_K, 𝔽₂), with multiplication of Brauer classes going to addition of cohomology classes; classically Br(K)[2] ≃ H²(G_K, μ₂). It is characterized by brauer2EquivH2_h2MuToUnits: followed by h2MuToUnits K, it is the comparison brauerCohomologyEquiv K on 2-torsion classes; see brauer2EquivH2_unique.

Equations

• TauCeti.brauer2EquivH2 K = (AddEquiv.ofBijective (TauCeti.h2ToTwoTorsion✝ K) ⋯).symm

@[simp]

theorem TauCeti.brauer2EquivH2_symm_apply (K : Type) [Field K] [Invertible 2] (y : ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) : ↑(Additive.toMul ((brauer2EquivH2 K).symm y)) = Additive.toMul ((brauerCohomologyEquiv K).symm ((TopModuleCat.Hom.hom (h2MuToUnits K)) y))

The inverse identification sends a class y of H²_cont(G_K, 𝔽₂) to the Brauer class that the comparison brauerCohomologyEquiv K matches with h2MuToUnits K y.

@[simp]

theorem TauCeti.brauer2EquivH2_h2MuToUnits {K : Type} [Field K] [Invertible 2] (x : ↥(BrauerGroup.twoTorsion K)) : (TopModuleCat.Hom.hom (h2MuToUnits K)) ((brauer2EquivH2 K) (Additive.ofMul x)) = (brauerCohomologyEquiv K) (Additive.ofMul ↑x)

The normalization of the 2-torsion comparison. On a 2-torsion Brauer class, brauer2EquivH2 K followed by h2MuToUnits K is the comparison brauerCohomologyEquiv K.

theorem TauCeti.brauer2EquivH2_unique {K : Type} [Field K] [Invertible 2] (e : Additive ↥(BrauerGroup.twoTorsion K) ≃+ ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) (h : ∀ (x : ↥(BrauerGroup.twoTorsion K)), (TopModuleCat.Hom.hom (h2MuToUnits K)) (e (Additive.ofMul x)) = (brauerCohomologyEquiv K) (Additive.ofMul ↑x)) : e = brauer2EquivH2 K

The 2-torsion comparison is determined by its normalization. Any additive equivalence Br(K)[2] ≃ H²_cont(G_K, 𝔽₂) which, followed by h2MuToUnits K, is the comparison brauerCohomologyEquiv K on 2-torsion classes is brauer2EquivH2 K, because h2MuToUnits K is injective.