coboundariesOfIsMulCoboundary₂ — Mathlib

English

If f ∈ cocycles₂(Rep.ofMulDistribMulAction G M), then Additive.toMul ∘ f is 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-coboundary condition, produces a
2-coboundary for the representation on `M` induced by the `MulDistribMulAction`. -/
def coboundariesOfIsMulCoboundary₂ {f : G × G → M} (hf : IsMulCoboundary₂ f) :
    coboundaries₂ (Rep.ofMulDistribMulAction G M) :=
  ⟨f, hf.choose, funext fun g ↦ hf.choose_spec g.1 g.2⟩

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