truncateAugment_hom_f — Mathlib

English

In the isomorphism between truncation and the original, all degreewise isomorphism pieces are identities on the original degrees: the hom side acts as the identity on each X_i.

Русский

Части гомоморфизма изоморфизма между усечением и исходным комплексом являются тождественными на соответствующих степенях.

LaTeX

$$$\\text{truncateAugment}.hom.f_i = \\mathrm{id}_{C.X_i} \\quad \\forall i$$$

Lean4

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

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