English
The construction to turn a chain map to a single-object target into a chain complex is defined by taking the augmentation of C with the data from the single-map equivalence.
Русский
Определение преобразования цепного отображения в единичный нулевой комплекс через аугментацию C данными эквивалентности.
LaTeX
$$$\\text{toSingle}_0^{AsComplex}(C,X,f) := \\text{augment}(C, f, w)\\text{ with } w\\text{ from } toSingle₀Equiv$$$
Lean4
/-- The truncation of an `ℕ`-indexed cochain complex,
deleting the object at `0` and shifting everything else down.
-/
@[simps]
def truncate [HasZeroMorphisms V] : CochainComplex V ℕ ⥤ CochainComplex V ℕ
where
obj
C :=
{ X := fun i => C.X (i + 1)
d := fun i j => C.d (i + 1) (j + 1)
shape := fun i j w => by
apply C.shape
simpa }
map f := { f := fun i => f.f (i + 1) }
