boundariesOfIsBoundary₂ — Mathlib

English

A 2-boundary x is equivalent to the existence of a 3-parameter y with a weighted sum equal to x.

Русский

2-граничность x эквивалентна существованию y с тяготящей суммой, равной x.

LaTeX

$$$IsBoundary_2 x \iff \exists y : G \times G \times G \to_0 A,\; y.sum (\lambda g a, \; \text{single}(g.2.1,g.2.2) a - \text{single}(g.1 * g.2.1, g.2.2) (g.1 \cdot a) + \text{single}(g.1, g.2.1 * g.2.2) (g.1 \cdot a) -\n \text{single}(g.1, g.2.1) (g.1 \cdot a)) = x$$$

Lean4

/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G × G →₀ A` satisfying the 2-boundary condition, produces a 2-boundary for the
representation on `A` induced by the `DistribMulAction`. -/
@[simps]
def boundariesOfIsBoundary₂ (x : G × G →₀ A) (hx : IsBoundary₂ x) : boundaries₂ (Rep.ofDistribMulAction k G A) :=
  ⟨x, hx⟩

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