Cohomology classes of crossed-product cocycles

A TwoCocycle K L is the multiplicative form of an inhomogeneous 2-cocycle of Aut_K(L) with values in Lˣ. This file connects that explicit object to Mathlib's second group cohomology. The map TwoCocycle.cohomologyClass reads a crossed-product cocycle as a class in H²(Aut_K(L), Lˣ), and TwoCocycle.cohomologyClass_eq_iff proves that equality of classes is exactly the explicit coboundary relation already used by crossed products.

Consequently TwoCocycle.cohomologyClassEquiv identifies H²(Aut_K(L), Lˣ) with explicit 2-cocycles modulo TwoCocycle.Cohomologous. This is the finite-cohomology input needed to apply the Hilbert 90 injectivity theorem to the classification of crossed-product Brauer classes.

Universes

Mathlib's multiplicative interface to groupCohomology.cocycles₂ (cocyclesOfIsMulCocycle₂, coboundariesOfIsMulCoboundary₂, isMulCoboundary₂_of_mem_coboundaries₂) is stated for an acting group and coefficient group in Type. This comes from Mathlib's low-degree group cohomology, which requires the acting group to share the universe of the coefficient ring, here ℤ : Type. The underlying TwoCocycle and CrossedProduct definitions remain universe-polymorphic; only their comparison with groupCohomology has this restriction.

Main results

• TauCeti.TwoCocycle.toCocycles₂: the additive 2-cocycle underlying an explicit crossed-product cocycle.
• TauCeti.TwoCocycle.cohomologyClass: its class in H²(Aut_K(L), Lˣ).
• TauCeti.TwoCocycle.cohomologyClass_eq_iff: two explicit cocycles determine the same class exactly when they are cohomologous.
• TauCeti.TwoCocycle.cohomologyClassEquiv: second cohomology classifies explicit cocycles modulo the cohomologous relation.

References

The construction adapts the factor-set classification of TauCeti/GroupTheory/GroupExtension/Cohomology.lean (TauCeti.FactorSet.toCocycles₂, TauCeti.FactorSet.cohomologyClass_eq_iff, TauCeti.FactorSet.cohomologyClassEquiv) from normalized factor sets of an arbitrary group to the unnormalized cocycles of Aut_K(L) used by crossed products; since those cocycles are not normalized, no normalization step is needed for surjectivity.

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

def TauCeti.TwoCocycle.toCocycles₂ {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z : TwoCocycle K L) : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction (L ≃ₐ[K] L) Lˣ))

A crossed-product 2-cocycle, read as a 2-cocycle valued in Additive Lˣ.

Equations

• z.toCocycles₂ = groupCohomology.cocyclesOfIsMulCocycle₂ ⋯

@[simp]

theorem TauCeti.TwoCocycle.coe_toCocycles₂ {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z : TwoCocycle K L) : ⇑z.toCocycles₂ = fun (p : (L ≃ₐ[K] L) × L ≃ₐ[K] L) => Additive.ofMul (z.toFun p.1 p.2)

The additive cocycle underlying z evaluates to Additive.ofMul (z(σ, τ)).

noncomputable def TauCeti.TwoCocycle.cohomologyClass {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z : TwoCocycle K L) : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction (L ≃ₐ[K] L) Lˣ))

The class in H²(Aut_K(L), Lˣ) represented by a crossed-product 2-cocycle.

Equations

• z.cohomologyClass = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction (L ≃ₐ[K] L) Lˣ))) z.toCocycles₂

theorem TauCeti.TwoCocycle.cohomologyClass_def {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z : TwoCocycle K L) : z.cohomologyClass = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction (L ≃ₐ[K] L) Lˣ))) z.toCocycles₂

The cohomology class of z is the image of its underlying additive cocycle.

theorem TauCeti.TwoCocycle.coe_toCocycles₂_sub {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z w : TwoCocycle K L) : ⇑w.toCocycles₂ - ⇑z.toCocycles₂ = fun (p : (L ≃ₐ[K] L) × L ≃ₐ[K] L) => Additive.ofMul (w.toFun p.1 p.2 / z.toFun p.1 p.2)

The pointwise quotient of two multiplicative cocycles is the difference of their additive counterparts.

theorem TauCeti.TwoCocycle.cohomologyClass_eq_iff {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z w : TwoCocycle K L) : z.cohomologyClass = w.cohomologyClass ↔ z.Cohomologous w

Two crossed-product cocycles represent the same class in H²(Aut_K(L), Lˣ) exactly when they are cohomologous.

@[simp]

theorem TauCeti.TwoCocycle.cohomologous_iff_cohomologyClass_eq {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z w : TwoCocycle K L) : z.Cohomologous w ↔ z.cohomologyClass = w.cohomologyClass

The explicit cohomologous relation is equality of second cohomology classes.

theorem TauCeti.TwoCocycle.exists_cohomologyClass_eq {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (x : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction (L ≃ₐ[K] L) Lˣ))) : ∃ (z : TwoCocycle K L), z.cohomologyClass = x

Every class in H²(Aut_K(L), Lˣ) is represented by an explicit crossed-product 2-cocycle.

noncomputable def TauCeti.TwoCocycle.cohomologousSetoid (K L : Type) [CommSemiring K] [CommRing L] [Algebra K L] : Setoid (TwoCocycle K L)

The setoid of cohomologous crossed-product 2-cocycles, presented as the kernel of their cohomology class.

Equations

• TauCeti.TwoCocycle.cohomologousSetoid K L = Setoid.ker TauCeti.TwoCocycle.cohomologyClass

@[simp]

theorem TauCeti.TwoCocycle.cohomologousSetoid_apply {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] {z w : TwoCocycle K L} : (cohomologousSetoid K L) z w ↔ z.Cohomologous w

The relation of TwoCocycle.cohomologousSetoid is TwoCocycle.Cohomologous.

noncomputable def TauCeti.TwoCocycle.cohomologyClassEquiv (K L : Type) [CommSemiring K] [CommRing L] [Algebra K L] : Quotient (cohomologousSetoid K L) ≃ ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction (L ≃ₐ[K] L) Lˣ))

Second group cohomology classifies crossed-product 2-cocycles modulo coboundaries.

Equations

• TauCeti.TwoCocycle.cohomologyClassEquiv K L = Setoid.quotientKerEquivOfSurjective TauCeti.TwoCocycle.cohomologyClass ⋯

@[simp]

theorem TauCeti.TwoCocycle.cohomologyClassEquiv_apply_mk {K L : Type} [CommSemiring K] [CommRing L] [Algebra K L] (z : TwoCocycle K L) : (cohomologyClassEquiv K L) ⟦z⟧ = z.cohomologyClass

TwoCocycle.cohomologyClassEquiv sends the class of a cocycle to its cohomology class.