Scalar extension of a crossed-product class #
For a finite Galois extension E/K and an intermediate field L, scalar extension of
the crossed-product class of a cocycle c is the class of c.restrict L.
The existing embedding CrossedProduct.restrictHom identifies the restricted crossed
product with the centralizer of L in the original algebra. The centralizer theorem
then identifies its Brauer class with scalar extension. This supplies the algebraic
side of the restriction square for the Brauer–cohomology comparison.
References #
- J.-P. Serre, Local Fields, Chapter X, §5.
- P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, §4.4.
@[simp]
theorem
TauCeti.BrauerGroup.baseChange_crossedProductClass
{K L E : Type u}
[Field K]
[Field L]
[Field E]
[Algebra K L]
[Algebra K E]
[Algebra L E]
[IsScalarTower K L E]
[FiniteDimensional K E]
[IsGalois K E]
(c : TwoCocycle K E)
:
Scalar extension of a crossed-product Brauer class to an intermediate field is the class of the cocycle restricted to the automorphisms fixing that field. No normality assumption on the intermediate field over the original base is needed.