Naturality of the Brauer–cohomology comparison

For a finite separable extension L/K, scalar extension of Brauer classes corresponds under brauerCohomologyEquiv to restriction in absolute Galois cohomology. This holds for every Brauer class, without a quaternion presentation or a normality assumption on L/K. Restricting the comparison to two-torsion gives the corresponding square for brauer2EquivH2 with trivial mod-two coefficients.

The proof uses BrauerGroup.exists_galoisCocycle_brauerClass_eq_with_le to choose a crossed-product presentation over a finite Galois field containing the image of L. The restricted crossed product represents scalar extension by TauCeti.BrauerGroup.baseChange_crossedProductClass, and its cohomology class is restriction by TauCeti.brauerCohomologyEquiv_restrict_crossedProductClass. The two-torsion square then follows from the defining square of brauer2EquivH2 and injectivity and restriction compatibility of h2MuToUnits.

References

• J.-P. Serre, Local Fields, Chapter X, §5.
• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, §4.4.

theorem TauCeti.brauerCohomologyEquiv_baseChange {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (x : BrauerGroup K) : (brauerCohomologyEquiv L) (Additive.ofMul ((BrauerGroup.baseChange K L) x)) = (CategoryTheory.ConcreteCategory.hom (galoisResUnits K L σ 2)) ((brauerCohomologyEquiv K) (Additive.ofMul x))

Scalar extension of any Brauer class corresponds to restriction under the Brauer–cohomology comparison, for a finite separable extension embedded in Kˢ. The extension need not be normal.

theorem TauCeti.brauer2EquivH2_baseChange {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] (x : ↥(BrauerGroup.twoTorsion K)) : (brauer2EquivH2 L) (Additive.ofMul ((BrauerGroup.twoTorsionBaseChange K L) x)) = (CategoryTheory.ConcreteCategory.hom (galoisRes K L σ 2)) ((brauer2EquivH2 K) (Additive.ofMul x))

Scalar extension of any two-torsion Brauer class corresponds under ι to restriction of its mod-two Galois cohomology class.