English
Truncation shifts a chain complex by deleting the 0th degree and relabeling degrees by i → i+1.
Русский
Трuncate: удаляем нулевую степень из цепного комплекса и сдвигаем индексы i ↦ i+1.
LaTeX
$$$\mathrm{truncate} : \text{ChainComplex} \, V \, \mathbb{N} \to \text{ChainComplex} \, V \, \mathbb{N}$ that maps $(X_*,d_*)$ to $(X_{*+1},d_{*+1})$$$
Lean4
/-- The truncation of an `ℕ`-indexed chain complex,
deleting the object at `0` and shifting everything else down.
-/
@[simps]
def truncate [HasZeroMorphisms V] : ChainComplex V ℕ ⥤ ChainComplex 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 => C.shape _ _ <| by simpa }
map f := { f := fun i => f.f (i + 1) }
