augmentTruncate_hom_f_zero — Mathlib

English

The forward map component at degree 0 of the augmentTruncate is the identity on the corresponding object.

Русский

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

LaTeX

$$$(\\text{augmentTruncate } C)_{0}^{\\text{hom}} = \\mathrm{id}_{C.X_0}$$$

Lean4

@[simp]
theorem augmentTruncate_hom_f_zero (C : CochainComplex V ℕ) : (augmentTruncate C).hom.f 0 = 𝟙 (C.X 0) :=
  rfl

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