English
Let C be a chain complex indexed by natural numbers and X an object. Morphisms from the chain complex concentrated at X in degree 0 to C are in bijection with morphisms X → C.X 0. Concretely, the 0th component of a morphism from (single0 V).obj X to C is exactly the map X → C.X 0, and conversely a map X → C.X 0 extends to a morphism from the single-object complex to C.
Русский
Пусть C — цепной комплекс и X — объект. Морфизмы от цепного комплекса, концентрированного в X в нулевой степень, к C образуют биекцию с морфизмами X → C.X 0.
LaTeX
$$$((\mathrm{single}_0 V).\mathrm{obj} X \to C) \cong (X \to C.X_0)$$$
Lean4
/-- Morphisms from a single object chain complex with `X` concentrated in degree 0
to an `ℕ`-indexed chain complex `C` are the same as morphisms `f : X → C.X 0`.
-/
@[simps apply]
noncomputable def fromSingle₀Equiv (C : ChainComplex V ℕ) (X : V) : ((single₀ V).obj X ⟶ C) ≃ (X ⟶ C.X 0)
where
toFun f := f.f 0
invFun f := HomologicalComplex.mkHomFromSingle f (fun i hi => by simp at hi)
left_inv := by cat_disch
right_inv := by cat_disch
