augmentTruncate_inv_f_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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