cocyclesOfIsCocycle₂ — Mathlib

English

If f ∈ coboundaries2 (Rep.ofDistribMulAction k G A), then IsCoboundary2 f.

Русский

Если f ∈ coboundaries2 (Rep.ofDistribMulAction k G A), тогда IsCoboundary2 f.

LaTeX

$$$f \in \text{coboundaries}_2(\mathrm{Rep.ofDistribMulAction}\; k\; G\; A) \Rightarrow \text{IsCoboundary}_2 f$$$

Lean4

/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
`f : G × G → A` satisfying the 2-cocycle condition, produces a 2-cocycle for the representation on
`A` induced by the `DistribMulAction`. -/
@[simps]
def cocyclesOfIsCocycle₂ {f : G × G → A} (hf : IsCocycle₂ f) : cocycles₂ (Rep.ofDistribMulAction k G A) :=
  ⟨f, (mem_cocycles₂_iff (A := Rep.ofDistribMulAction k G A) f).2 hf⟩

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