coboundariesOfIsCoboundary₁ — Mathlib

English

Given f: G×G→A satisfying IsCocycle2, produce a cocycles2 element for Rep.ofDistribMulAction.

Русский

Заданная функция f при условии IsCocycle2 порождает кокцикл2 для Rep.ofDistribMulAction.

LaTeX

$$$\text{cocyclesOfIsCocycle}_2( f ) : \text{cocycles}_2(\mathrm{Rep.ofDistribMulAction}\; k\; G\; A)$$$

Lean4

/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
`f : G → A` satisfying the 1-coboundary condition, produces a 1-coboundary for the representation
on `A` induced by the `DistribMulAction`. -/
@[simps]
def coboundariesOfIsCoboundary₁ {f : G → A} (hf : IsCoboundary₁ f) : coboundaries₁ (Rep.ofDistribMulAction k G A) :=
  ⟨f, hf.choose, funext hf.choose_spec⟩

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