cocyclesOfIsCocycle₁ — Mathlib

English

If f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A), then IsCoboundary₂ f.

Русский

Если f ∈ coboundaries2 (Rep.ofDistribMulAction k G A), тогда IsCoboundary₂ 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 → A` satisfying the 1-cocycle condition, produces a 1-cocycle for the representation on
`A` induced by the `DistribMulAction`. -/
@[simps]
def cocyclesOfIsCocycle₁ {f : G → A} (hf : IsCocycle₁ f) : cocycles₁ (Rep.ofDistribMulAction k G A) :=
  ⟨f, (mem_cocycles₁_iff (A := Rep.ofDistribMulAction k G A) f).2 hf⟩

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