d_of — Mathlib

English

Explicit description of the differential in the standard resolution of k as a trivial G-representation: it sends a basis element corresponding to a tuple (g0,…,gn+1) to the alternating sum of its faces.

Русский

Явное описание дифференциала в стандартном резолюционном комплексе над k как тривиального представления G: он отправляет базисный элемент, соответствующий кортежу (g0,…,gn+1), на чередующуюся сумму лиц.

LaTeX

$$$d_{n+1,n}( (g_0,\\dots,g_{n+1}) ) = \\sum_{i=0}^{n} (-1)^i (g_0,\\dots, \\widehat{g_i}, \\dots, g_{n+1}).$$$

Lean4

@[simp]
theorem d_of {G : Type u} {n : ℕ} (c : Fin (n + 1) → G) :
    d k G n (Finsupp.single c 1) =
      Finset.univ.sum fun p : Fin (n + 1) => Finsupp.single (c ∘ p.succAbove) ((-1 : k) ^ (p : ℕ)) :=
  by simp [d]

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