The cocycle of a splitting recovers the class of the algebra being split

Let L/K be a finite Galois extension and A a finite-dimensional central simple K-algebra with a splitting φ : L ⊗[K] A ≃ₐ[L] Mₙ(L). This file proves that the crossed product of the cocycle c = cocycleOfSplitting φ has the Brauer class of A, and deduces that every central simple algebra split by L has the class of a crossed product over L.

Together with the existence of finite Galois splitting fields, this shows that every Brauer class of K is the class of a crossed product, i.e. that the crossed-product construction from Galois 2-cocycles to the Brauer group is surjective.

Main results

• TauCeti.BrauerGroup.crossedProductClass_cocycleOfSplitting: the crossed product of the cocycle attached to a splitting of A has the Brauer class of A.
• TauCeti.BrauerGroup.exists_crossedProductClass_eq_of_isSplittingField: every central simple algebra split by a finite Galois L/K has the Brauer class of a crossed product over L.

References

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

theorem TauCeti.BrauerGroup.crossedProductClass_cocycleOfSplitting {K : Type u} [Field K] {A : Type u} [Ring A] [Algebra K A] {L : Type u} [Field L] [Algebra K L] {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [FiniteDimensional K L] [IsGalois K L] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : crossedProductClass (cocycleOfSplitting φ) = mk (CSA.of K A)

The cocycle of a splitting recovers the class of the algebra being split. For a finite Galois L/K and a splitting φ : L ⊗[K] A ≃ₐ[L] Mₙ(L) of a finite-dimensional central simple K-algebra A, the crossed product of cocycleOfSplitting φ is Brauer equivalent to A.

theorem TauCeti.BrauerGroup.exists_crossedProductClass_eq_of_isSplittingField {K : Type u} [Field K] {A : Type u} [Ring A] [Algebra K A] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (h : Algebra.IsSplittingField K A L) : ∃ (c : TwoCocycle K L), crossedProductClass c = mk (CSA.of K A)

Every algebra split by a finite Galois extension is a crossed product up to Brauer equivalence: if L/K is finite Galois and splits the finite-dimensional central simple K-algebra A, then some 2-cocycle of Gal(L/K) has the Brauer class of A, namely the cocycle of any splitting.