English
A 2-boundary x is characterised by an auxiliary y with a specified 4-term sum equalling 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) - \text{single}(g.1,g.2.1)(g.1 \cdot a)) = x$$$
Lean4
theorem isBoundary₂_iff (x : G × G →₀ A) :
IsBoundary₂ x ↔
∃ y : G × G × G →₀ A,
y.sum
(fun g a =>
single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
single (g.1, g.2.1) (g.1 • a)) =
x :=
by
constructor
· rintro ⟨y, hy⟩
use y.sum (fun g a => single g (g.1⁻¹ • a))
simp_all [sum_sum_index]
· rintro ⟨x, hx⟩
use x.sum (fun g a => single g (g.1 • a))
simp_all [sum_sum_index]
