Cohomologous cocycles give isomorphic crossed products

Two 2-cocycles z and w of Aut_K(L) with values in Lˣ are cohomologous when they differ by the coboundary of a function b : Aut_K(L) → Lˣ: w(σ, τ) = z(σ, τ) · σ(b(τ)) · b(στ)⁻¹ · b(σ). In Mathlib's language this says that the pointwise quotient w / z satisfies groupCohomology.IsMulCoboundary₂, and that is how TauCeti.TwoCocycle.Cohomologous is defined; TauCeti.TwoCocycle.cohomologous_iff is the explicit formula.

The crossed products of cohomologous cocycles are isomorphic as K-algebras: the L-linear map u'_σ ↦ b(σ) · u_σ from the crossed product of w to that of z is multiplicative, because (b(σ) · u_σ) · (b(τ) · u_τ) = (b(σ) · σ(b(τ)) · z(σ, τ)) · u_{στ} = (w(σ, τ) · b(στ)) · u_{στ} is its value on u'_σ · u'_τ = w(σ, τ) · u'_{στ}.

Main definitions

• TauCeti.TwoCocycle.Cohomologous z w: the cocycles z and w differ by a coboundary.
• TauCeti.CrossedProduct.algEquivOfCoboundary b h: for w / z the coboundary of b, the L-linear K-algebra isomorphism CrossedProduct w ≃ₐ[K] CrossedProduct z sending u'_σ to b(σ) · u_σ.

Main results

• TauCeti.TwoCocycle.cohomologous_iff: being cohomologous, as the explicit formula in L.
• TauCeti.TwoCocycle.Cohomologous.refl, .symm, .trans: it is an equivalence relation.
• TauCeti.TwoCocycle.cohomologous_iff_one_cohomologous_div: z and w are cohomologous exactly when w / z is cohomologous to the trivial cocycle.
• TauCeti.TwoCocycle.Cohomologous.comap: inflation along a compatible pair preserves being cohomologous.
• TauCeti.CrossedProduct.nonempty_algEquiv_of_cohomologous: the crossed products of cohomologous cocycles are isomorphic K-algebras.

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.

def TauCeti.TwoCocycle.Cohomologous {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (z w : TwoCocycle K L) : Prop

Two 2-cocycles z and w are cohomologous when their pointwise quotient w / z is a multiplicative 2-coboundary, that is w(σ, τ) = z(σ, τ) · σ(b(τ)) · b(στ)⁻¹ · b(σ) for some b : Aut_K(L) → Lˣ; see TwoCocycle.cohomologous_iff.

Equations

• z.Cohomologous w = groupCohomology.IsMulCoboundary₂ fun (p : (L ≃ₐ[K] L) × L ≃ₐ[K] L) => w.toFun p.1 p.2 / z.toFun p.1 p.2

theorem TauCeti.TwoCocycle.cohomologous_def {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} : z.Cohomologous w ↔ groupCohomology.IsMulCoboundary₂ fun (p : (L ≃ₐ[K] L) × L ≃ₐ[K] L) => w.toFun p.1 p.2 / z.toFun p.1 p.2

The explicit multiplicative coboundary predicate underlying TwoCocycle.Cohomologous.

theorem TauCeti.TwoCocycle.cohomologous_iff {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} : z.Cohomologous w ↔ ∃ (b : (L ≃ₐ[K] L) → Lˣ), ∀ (σ τ : L ≃ₐ[K] L), ↑(w.toFun σ τ) = ↑(z.toFun σ τ) * σ ↑(b τ) * ↑(b (σ * τ))⁻¹ * ↑(b σ)

The cocycles z and w are cohomologous if and only if w(σ, τ) = z(σ, τ) · σ(b(τ)) · b(στ)⁻¹ · b(σ) for some b : Aut_K(L) → Lˣ.

theorem TauCeti.TwoCocycle.Cohomologous.refl {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (z : TwoCocycle K L) : z.Cohomologous z

Every cocycle is cohomologous to itself.

theorem TauCeti.TwoCocycle.Cohomologous.symm {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} (h : z.Cohomologous w) : w.Cohomologous z

Being cohomologous is symmetric.

theorem TauCeti.TwoCocycle.Cohomologous.trans {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w v : TwoCocycle K L} (h₁ : z.Cohomologous w) (h₂ : w.Cohomologous v) : z.Cohomologous v

Being cohomologous is transitive.

theorem TauCeti.TwoCocycle.cohomologous_iff_one_cohomologous_div {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} : z.Cohomologous w ↔ Cohomologous 1 (w / z)

Two cocycles are cohomologous exactly when their quotient is cohomologous to the trivial cocycle, that is, when w / z is a coboundary.

theorem TauCeti.TwoCocycle.Cohomologous.comap {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) {z w : TwoCocycle K L} (h : z.Cohomologous w) : (TwoCocycle.comap f ι hf z).Cohomologous (TwoCocycle.comap f ι hf w)

Inflation preserves being cohomologous: if w / z is the coboundary of b, then the inflation of w / z is the coboundary of g ↦ ι (b (f g)).

noncomputable def TauCeti.CrossedProduct.algEquivOfCoboundary {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} (b : (L ≃ₐ[K] L) → Lˣ) (h : ∀ (σ τ : L ≃ₐ[K] L), σ • b τ / b (σ * τ) * b σ = w.toFun σ τ / z.toFun σ τ) : CrossedProduct w ≃ₐ[K] CrossedProduct z

Cohomologous cocycles have isomorphic crossed products. If w / z is the coboundary of b : Aut_K(L) → Lˣ, that is w(σ, τ) = z(σ, τ) · σ(b(τ)) · b(στ)⁻¹ · b(σ), then x · u'_σ ↦ (x · b(σ)) · u_σ is an isomorphism of K-algebras from the crossed product of w to that of z.

Equations

• TauCeti.CrossedProduct.algEquivOfCoboundary b h = AlgEquiv.ofLinearEquiv (LinearEquiv.restrictScalars K (TauCeti.CrossedProduct.linearEquivOfCoboundary✝ z w b)) ⋯ ⋯

@[simp]

theorem TauCeti.CrossedProduct.algEquivOfCoboundary_basis {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} (b : (L ≃ₐ[K] L) → Lˣ) (h : ∀ (σ τ : L ≃ₐ[K] L), σ • b τ / b (σ * τ) * b σ = w.toFun σ τ / z.toFun σ τ) (σ : L ≃ₐ[K] L) : (algEquivOfCoboundary b h) ((basis w) σ) = ↑(b σ) • (basis z) σ

CrossedProduct.algEquivOfCoboundary sends u'_σ to b(σ) · u_σ.

@[simp]

theorem TauCeti.CrossedProduct.algEquivOfCoboundary_smul {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} (b : (L ≃ₐ[K] L) → Lˣ) (h : ∀ (σ τ : L ≃ₐ[K] L), σ • b τ / b (σ * τ) * b σ = w.toFun σ τ / z.toFun σ τ) (x : L) (a : CrossedProduct w) : (algEquivOfCoboundary b h) (x • a) = x • (algEquivOfCoboundary b h) a

CrossedProduct.algEquivOfCoboundary is L-linear.

@[simp]

theorem TauCeti.CrossedProduct.algEquivOfCoboundary_inc {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} (b : (L ≃ₐ[K] L) → Lˣ) (h : ∀ (σ τ : L ≃ₐ[K] L), σ • b τ / b (σ * τ) * b σ = w.toFun σ τ / z.toFun σ τ) (x : L) : (algEquivOfCoboundary b h) ((inc w) x) = (inc z) x

CrossedProduct.algEquivOfCoboundary restricts to the identity on the embedded copies of L.

@[simp]

theorem TauCeti.CrossedProduct.repr_algEquivOfCoboundary {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} (b : (L ≃ₐ[K] L) → Lˣ) (h : ∀ (σ τ : L ≃ₐ[K] L), σ • b τ / b (σ * τ) * b σ = w.toFun σ τ / z.toFun σ τ) (a : CrossedProduct w) (σ : L ≃ₐ[K] L) : ((basis z).repr ((algEquivOfCoboundary b h) a)) σ = ((basis w).repr a) σ * ↑(b σ)

The coordinates of CrossedProduct.algEquivOfCoboundary b h a are those of a, the σ-th one multiplied by b(σ).

theorem TauCeti.CrossedProduct.nonempty_algEquiv_of_cohomologous {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {z w : TwoCocycle K L} (hzw : z.Cohomologous w) : Nonempty (CrossedProduct z ≃ₐ[K] CrossedProduct w)

The crossed products of cohomologous cocycles are isomorphic K-algebras.