augmentTruncate_hom_f_succ — Mathlib

English

The forward map component at degree i+1 of the augmentation is the identity on the corresponding object.

Русский

Компонент отображения вперед на степени i+1 является тождественным на соответствующем объекте.

LaTeX

$$$(\\text{augmentTruncate } C)_{i+1}^{\\text{hom}} = \\mathrm{id}_{C.X_{i+1}}$$$

Lean4

@[simp]
theorem augmentTruncate_hom_f_succ (C : CochainComplex V ℕ) (i : ℕ) :
    (augmentTruncate C).hom.f (i + 1) = 𝟙 (C.X (i + 1)) :=
  rfl

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