English
For a morphism f: C.X0 ⟶ X, applying the inverse of the toSingle₀Equiv pairing yields a |0| component equal to f.
Русский
Для морфизма f: C.X0 ⟶ X, применение обратного отображения toSingle₀Equiv даёт нулевую компоненту равную f.
LaTeX
$$$((\\mathrm{toSingle}_0^{\\mathrm{Equiv}} C X)^{-1} f)_0 = f$$$
Lean4
/-- Morphisms to a single object cochain complex with `X` concentrated in degree 0
to an `ℕ`-indexed cochain complex `C` are the same as morphisms `f : C.X 0 ⟶ X`.
-/
@[simps apply]
noncomputable def toSingle₀Equiv (C : CochainComplex V ℕ) (X : V) : (C ⟶ (single₀ V).obj X) ≃ (C.X 0 ⟶ X)
where
toFun f := f.f 0
invFun f := HomologicalComplex.mkHomToSingle f (fun i hi => by simp at hi)
left_inv := by cat_disch
right_inv := by cat_disch
