d_single — Mathlib

English

In the bar complex, the image of a single basis element under the differential is the sum of a primary component and a tail given by contractNth.

Русский

В бар-комплексе образ базисного элемента под дифференциалом есть сумма главной составляющей и хвоста по формуле contractNth.

LaTeX

$$$d\\, (\\text{single } x) = \\text{single}(x_i.succ) + \\sum_j \\text{single}(\\mathrm{contractNth}(j,x))$$$

Lean4

theorem d_single (x : Gⁿ⁺¹) :
    (d k G n).hom (single x (single 1 1)) =
      single (fun i => x i.succ) (Finsupp.single (x 0) 1) +
        Finset.univ.sum fun j : Fin (n + 1) =>
          single (Fin.contractNth j (· * ·) x) (single (1 : G) ((-1 : k) ^ ((j : ℕ) + 1))) :=
  by simp [d]

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