cocyclesOfIsMulCocycle₂ — Mathlib

English

If f ∈ cocycles₂(Rep.ofMulDistribMulAction G M), then Additive.toMul ∘ f is a IsMulCocycle₂.

Русский

Если f ∈ cocycles₂(Rep.ofMulDistribMulAction G M), то Additive.toMul ∘ f является IsMulCocycle₂.

LaTeX

$$$f \\in cocycles_2(Rep.ofMulDistribMulAction\\ G\\ M) \\Rightarrow IsMulCocycle_2(\\text{Additive.toMul} \\circ f)$$$

Lean4

/-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
`f : G × G → M` satisfying the multiplicative 2-cocycle condition, produces a 2-cocycle for the
representation on `Additive M` induced by the `MulDistribMulAction`. -/
@[simps]
def cocyclesOfIsMulCocycle₂ {f : G × G → M} (hf : IsMulCocycle₂ f) : cocycles₂ (Rep.ofMulDistribMulAction G M) :=
  ⟨Additive.ofMul ∘ f, (mem_cocycles₂_iff (A := Rep.ofMulDistribMulAction G M) f).2 hf⟩

Похожие утверждения