coboundariesOfIsMulCoboundary₁ — Mathlib

English

Given f: G → M with IsMulCoboundary₁ f, coboundaries₁(Rep.ofMulDistribMulAction G M) contains (f, x) where x witnesses the coboundary condition.

Русский

Пусть f: G → M удовлетворяет IsMulCoboundary₁ f; тогда coboundaries₁(Rep.ofMulDistribMulAction G M) содержит тройку (f, x), где x свидетельствует условие кобунданд.

LaTeX

$$∃ x: G → M, ∀ g h: G, g • x h / x (g h) * x g = f (g, h)$$

Lean4

/-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
`f : G → M` satisfying the multiplicative 1-coboundary condition, produces a
1-coboundary for the representation on `Additive M` induced by the `MulDistribMulAction`. -/
@[simps]
def coboundariesOfIsMulCoboundary₁ {f : G → M} (hf : IsMulCoboundary₁ f) :
    coboundaries₁ (Rep.ofMulDistribMulAction G M) :=
  ⟨f, hf.choose, funext hf.choose_spec⟩

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