English
A chain map from a chain complex to the single-object zero-th degree complex can be reinterpreted as a chain complex via augmentation with a suitable morphism and relation.
Русский
Любое цепное отображение в единичный нулевой степени комплекс можно переинтерпретировать как цепной комплекс через аугментацию и соответствующее отношение.
LaTeX
$$$\\text{toSingle}_0^{AsComplex}(C,X,f) := \\text{augment}(C, f, w) \\text{ with } w: C.d_{1 0} \\circ f = 0$$$
Lean4
/-- A chain map from a chain complex to a single object chain complex in degree zero
can be reinterpreted as a chain complex.
This is the inverse construction of `truncateTo`.
-/
def toSingle₀AsComplex [HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (f : C ⟶ (single₀ V).obj X) :
ChainComplex V ℕ :=
let ⟨f, w⟩ := toSingle₀Equiv C X f
augment C f w
