isBoundary₁_iff — Mathlib

English

An element x ∈ C¹ is a boundary of level 1 iff there exists y: G×G →₀ A with a specified triple-sum expression equal to x.

Русский

Элемент x ∈ C¹ является границей первого уровня тогда и только тогда, существует y: G×G →₀ A со строкой тройной суммы, равной x.

LaTeX

$$$\\text{IsBoundary}_1(x) \\iff \\exists y : G \\times G \\to₀ A, \\, y.sum (\\lambda g a, (g, a) \\mapsto ...) = x$$$

Lean4

theorem isBoundary₁_iff (x : G →₀ A) :
    IsBoundary₁ x ↔
      ∃ y : G × G →₀ A, y.sum (fun g a => single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.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]

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