Every Brauer class is a crossed-product class

A TauCeti.GaloisCocycle K bundles a finite Galois subextension L of the separable closure Kˢ/K with a 2-cocycle of Gal(L/K) with values in Lˣ; its Brauer class is the class of the crossed product of its cocycle.

Every Brauer class of K is the class of the crossed product of such a bundled cocycle: a finite-dimensional central simple K-algebra A is split by a finite Galois subextension of Kˢ/K (TauCeti.Algebra.exists_finiteGalois_splittingField), and the crossed product of the cocycle attached to a splitting has the class of A (TauCeti.BrauerGroup.crossedProductClass_cocycleOfSplitting).

Main definitions

• TauCeti.GaloisCocycle.brauerClass: the Brauer class of its crossed product.

Main results

• TauCeti.BrauerGroup.exists_galoisCocycle_brauerClass_eq: every Brauer class of K is the class of a bundled Galois cocycle.

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.

noncomputable def TauCeti.GaloisCocycle.brauerClass {K : Type u} [Field K] (g : GaloisCocycle K) : BrauerGroup K

The Brauer class of a Galois cocycle: the class of the crossed product of its cocycle.

Equations

• g.brauerClass = TauCeti.BrauerGroup.crossedProductClass g.cocycle

@[simp]

theorem TauCeti.GaloisCocycle.brauerClass_def {K : Type u} [Field K] (g : GaloisCocycle K) : g.brauerClass = BrauerGroup.crossedProductClass g.cocycle

The Brauer class of a Galois cocycle is the crossed-product class of its cocycle.

theorem TauCeti.BrauerGroup.exists_galoisCocycle_brauerClass_eq {K : Type u} [Field K] (x : BrauerGroup K) : ∃ (g : GaloisCocycle K), g.brauerClass = x

Every Brauer class is obtained from a Galois cocycle: each class of Br(K) is the class of the crossed product of a 2-cocycle of a finite Galois subextension of Kˢ/K.