d_single — Mathlib

English

Explicitly describes the differential on a single generator in the inhomogeneous chains.

Русский

Явное описание оператора разности на одиногенераторе в неоднородных цепях.

LaTeX

$$d_A_n(single g a) = single (\lambda i => g i.succ)(A.\rho(g 0)^{-1} a) + \sum_{j} (-1)^{(j+1)} • single (Fin.contractNth j (·*·) g) a$$

Lean4

@[simp]
theorem d_single (n : ℕ) (g : Fin (n + 1) → G) (a : A) :
    d A n (single g a) =
      single (fun i => g i.succ) (A.ρ (g 0)⁻¹ a) +
        Finset.univ.sum fun j : Fin (n + 1) => (-1 : k) ^ ((j : ℕ) + 1) • single (Fin.contractNth j (· * ·) g) a :=
  by simp [d]

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