truncateAugment_hom_f — Mathlib

English

All inverse components for the truncate-augment isomorphism are identities on all degrees.

Русский

Все компоненты обратного изоморфизма тождественны на всех степенях.

LaTeX

$$$\\forall i:\\ N,\\ (\\text{truncateAugment}.inv.f_{i+1}) = \\mathrm{id}_{(\\text{truncate.obj } (\\text{augment } C f w)).X_{i+1}}$$$

Lean4

@[simp]
theorem truncateAugment_hom_f (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i : ℕ) :
    (truncateAugment C f w).hom.f i = 𝟙 (C.X i) :=
  rfl

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