The cohomology class of a restricted crossed product

Let E/K be finite Galois inside Kˢ, and let L be an intermediate scalar field, embedded by σ : L →ₐ[K] Kˢ compatibly with the scalar action on E. Restricting a cocycle of Aut_K(E) to Aut_L(E) gives a crossed product over L. Its image under brauerCohomologyEquiv L is the restriction of the original inflated cohomology class.

The statement does not require L/K to be normal. To evaluate the comparison over L, the finite Galois extension E/L is transported into Lˢ; both its crossed-product class and its inflated class are preserved by this transport. Combined with the centralizer description of CrossedProduct.restrictHom, this supplies the cohomological side of scalar-extension naturality of the Brauer comparison.

References

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

theorem TauCeti.instFiniteDimensionalSubtypeSeparableClosureMemIntermediateField_tauCeti {K L : Type u} [Field K] [Field L] [Algebra K L] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [Algebra L ↥E] [IsScalarTower K L ↥E] : FiniteDimensional L ↥E

theorem TauCeti.instIsGaloisSubtypeSeparableClosureMemIntermediateField_tauCeti {K L : Type u} [Field K] [Field L] [Algebra K L] (E : IntermediateField K (SeparableClosure K)) [IsGalois K ↥E] [Algebra L ↥E] [IsScalarTower K L ↥E] : IsGalois L ↥E

theorem TauCeti.brauerCohomologyEquiv_restrict_crossedProductClass {K L : Type u} [Field K] [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [IsGalois K ↥E] [Algebra L ↥E] [IsScalarTower K L ↥E] (hσ : ∀ (x : L), E.val ((algebraMap L ↥E) x) = σ x) (c : TwoCocycle K ↥E) : (brauerCohomologyEquiv L) (Additive.ofMul (BrauerGroup.crossedProductClass (c.restrict L))) = (CategoryTheory.ConcreteCategory.hom (galoisResUnits K L σ 2)) ((brauerCohomologyEquiv K) (Additive.ofMul (BrauerGroup.crossedProductClass c)))

The Brauer comparison commutes with restricting a finite Galois cocycle to the automorphisms fixing an intermediate scalar field, even when L/K is not normal.