Equal crossed-product classes come from cohomologous cocycles

For a finite Galois extension L/K, the Brauer class of the crossed product (L, Gal(L/K), c) determines the cocycle c up to coboundaries: if two cocycles z and w have the same Brauer class, then they are cohomologous. Together with TauCeti.BrauerGroup.crossedProductClass_eq_of_cohomologous this says that the crossed-product construction is injective on cocycles modulo coboundaries, which is the injectivity half of the comparison between H²(Gal(L/K), Lˣ) and the relative Brauer group of L/K.

Since crossedProductClass is multiplicative (TauCeti.BrauerGroup.crossedProductClass_mul), it suffices to show that a cocycle c whose crossed product is split is a coboundary. The argument is a dimension count. A split crossed product A = (L, Gal(L/K), c) of dimension [L : K]² is a matrix algebra M_n(K) with n = [L : K], so it acts on a K-vector space V of dimension [L : K]. Restricted to L ⊆ A, this makes V a one-dimensional L-vector space, so V = L · v for any v ≠ 0. Each u_σ acts σ-semilinearly, hence u_σ · v = b(σ) · v for a unique b(σ) ∈ Lˣ, and expanding u_σ · u_τ · v = c(σ, τ) · u_{στ} · v gives c(σ, τ) = σ(b(τ)) · b(στ)⁻¹ · b(σ).

Main results

• TauCeti.TwoCocycle.one_cohomologous_of_algHom_end: a cocycle whose crossed product acts on a K-vector space of dimension [L : K] is a coboundary.
• TauCeti.BrauerGroup.crossedProductClass_one: the trivial cocycle presents the identity class.
• TauCeti.BrauerGroup.crossedProductClass_eq_one_iff: a crossed product is split exactly when its cocycle is a coboundary.
• TauCeti.BrauerGroup.crossedProductClass_eq_iff, TauCeti.BrauerGroup.cohomologous_of_crossedProductClass_eq: two cocycles have the same Brauer class exactly when they are cohomologous.

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, §5.

theorem TauCeti.TwoCocycle.one_cohomologous_of_algHom_end {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] [FiniteDimensional K L] {V : Type u_1} [AddCommGroup V] [Module K V] (c : TwoCocycle K L) (ρ : CrossedProduct c →ₐ[K] Module.End K V) (hV : Module.finrank K V = Module.finrank K L) : Cohomologous 1 c

A crossed product with a module of dimension [L : K] has a trivial cocycle. If the crossed product of c acts K-linearly on a K-vector space V with dim_K V = [L : K], then c is a coboundary: c(σ, τ) = σ(b(τ)) · b(στ)⁻¹ · b(σ) for some b : Aut_K(L) → Lˣ. No Galois hypothesis is needed.

@[simp]

theorem TauCeti.BrauerGroup.crossedProductClass_one {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : crossedProductClass 1 = 1

The trivial cocycle presents the identity Brauer class: the crossed product of the trivial cocycle of a finite Galois extension is split.

theorem TauCeti.BrauerGroup.crossedProductClass_eq_one_iff {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {c : TwoCocycle K L} : crossedProductClass c = 1 ↔ TwoCocycle.Cohomologous 1 c

A crossed product is split exactly when its cocycle is a coboundary.

theorem TauCeti.BrauerGroup.crossedProductClass_eq_iff {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {z w : TwoCocycle K L} : crossedProductClass z = crossedProductClass w ↔ z.Cohomologous w

Equal crossed-product classes come from cohomologous cocycles, and conversely.

theorem TauCeti.BrauerGroup.cohomologous_of_crossedProductClass_eq {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {z w : TwoCocycle K L} (h : crossedProductClass z = crossedProductClass w) : z.Cohomologous w

Injectivity of the crossed-product construction. Two cocycles of a finite Galois extension whose crossed products have the same Brauer class are cohomologous. The converse is TauCeti.BrauerGroup.crossedProductClass_eq_of_cohomologous.