truncateAugment_inv_f — Mathlib

English

There is an isomorphism between the truncated augmented cochain complex and the original cochain complex, with identity maps on all places.

Русский

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

LaTeX

$$$\\text{truncateAugment} : (\\text{augment } C f w) \\to C$ is an isomorphism with identity components$$

Lean4

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

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