English
There is a canonical chain map from the truncated complex to the single-object complex in degree 0, given by the differential C.d_{1,0} and zero elsewhere.
Русский
Существет каноничное отображение цепного комплекса после усечения в кратный комплекс к однообъектному в степени 0, компонента у нулевой степени задана дифференциалом C.d_{1,0}, а остальное нули.
LaTeX
$$$\mathrm{truncateTo} : \mathrm{truncate.obj}(C) \to (\mathrm{single₀} V).obj (C.X 0)$ с компонентами $\langle C.d_{1 0}, 0, 0, \dots \rangle$$$
Lean4
/-- There is a canonical chain map from the truncation of a chain map `C` to
the "single object" chain complex consisting of the truncated object `C.X 0` in degree 0.
The components of this chain map are `C.d 1 0` in degree 0, and zero otherwise.
-/
def truncateTo [HasZeroObject V] [HasZeroMorphisms V] (C : ChainComplex V ℕ) :
truncate.obj C ⟶ (single₀ V).obj (C.X 0) :=
(toSingle₀Equiv (truncate.obj C) (C.X 0)).symm
⟨C.d 1 0, by simp⟩
-- PROJECT when `V` is abelian (but not generally?)
-- `[∀ n, Exact (C.d (n+2) (n+1)) (C.d (n+1) n)] [Epi (C.d 1 0)]` iff `QuasiIso (C.truncate_to)`
