augment_X_zero — Mathlib

English

Augmenting a truncated chain complex by reinserting the original object and morphism yields a chain complex isomorphic to the original.

Русский

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

LaTeX

$$$\\text{augmentTruncate}(C) : \\; (\\text{truncate.obj } C) \\uparrow \\simeq C$$$

Lean4

@[simp]
theorem augment_X_zero (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
    (augment C f w).X 0 = X :=
  rfl

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