cyclesOfIsCycle₁ — Mathlib

English

A 2-variable function is a 2-boundary iff there exists a 3-variable function whose alternating boundary equals the function.

Русский

Функция из G×G является 2-граничностью тогда и только тогда, когда существует функция из G×G×G, чья чередующая граница равна данной функции.

LaTeX

$$$IsBoundary_2 x \iff \exists y : G \times G \times G \to_0 A,\; y.sum (\lambda g a, \; \text{...}) = x$$$

Lean4

/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G →₀ A` satisfying the 1-cycle condition, produces a 1-cycle for the representation on
`A` induced by the `DistribMulAction`. -/
@[simps]
def cyclesOfIsCycle₁ (x : G →₀ A) (hx : IsCycle₁ x) : cycles₁ (Rep.ofDistribMulAction k G A) :=
  ⟨x, (mem_cycles₁_iff (A := Rep.ofDistribMulAction k G A) x).2 hx⟩

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