normalizedMooreComplex_objD — Mathlib

English

The differential d at level n of the normalized Moore complex equals the pre-defined objD X n from the construction, i.e., ((normalizedMooreComplex).obj X).d (n+1) n = NormalizedMooreComplex.objD X n.

Русский

Дифференциал уровня n нормализованного Moore-комплекса совпадает с заданным objD X n; то есть ((normalizedMooreComplex).obj X).d (n+1) n = NormalizedMooreComplex.objD X n.

LaTeX

$$$ ((\\mathrm{normalizedMooreComplex}\\,C).\\mathrm{obj}\,X).d (n+1)\\;n = \\mathrm{NormalizedMooreComplex.objD}\\ X\\ n $$$

Lean4

theorem normalizedMooreComplex_objD (X : SimplicialObject C) (n : ℕ) :
    ((normalizedMooreComplex C).obj X).d (n + 1) n = NormalizedMooreComplex.objD X n :=
  ChainComplex.of_d _ _ (d_squared X) n

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