English
The augmentation of a truncated cochain complex is canonically isomorphic to the original complex, with all identity components.
Русский
Аугментированное усечение когомологического комплекса канонически изоморфно исходному комплексу, все компоненты идентичны.
LaTeX
$$$\\operatorname{augmentTruncate}(C) \\cong C$$$
Lean4
/-- Augmenting a truncated complex with the original object and morphism is isomorphic
(with components the identity) to the original complex.
-/
def augmentTruncate (C : CochainComplex V ℕ) : augment (truncate.obj C) (C.d 0 1) (C.d_comp_d _ _ _) ≅ C
where
hom :=
{ f := fun
| 0 => 𝟙 _
| _ + 1 => 𝟙 _
comm' := fun i j => by rcases j with (_ | _ | j) <;> cases i <;> aesop }
inv :=
{ f := fun
| 0 => 𝟙 _
| _ + 1 => 𝟙 _
comm' := fun i j => by rcases j with (_ | _ | j) <;> rcases i with - | i <;> aesop }
