English
Let C be a chain complex indexed by the natural numbers in a category with zero morphisms and a zero object, and let X be an object of that category. Then the set of morphisms from C to the chain complex that concentrates X in degree 0 is in natural bijection with the set of morphisms f: C.X 0 → X satisfying the compatibility condition C.d 1 0 ≫ f = 0 (i.e., the horizontal differential into degree 0 followed by f vanishes).
Русский
Пусть C — цепной комплекс, индексируемый по натуральным числам, в категории с нулевыми морфизмами и нулевым объектом; пусть X — объект. Тогда множество морфизмов из C в цепной комплекс, концентраированный в нулевой степени в X, гомотетически эквивалентно множеству морфизмов f: C.X 0 → X, удовлетворяющим условию совместимости C.d 1 0 ≫ f = 0.
LaTeX
$$$\operatorname{Hom}(C, \mathrm{single}_0 X) \cong \{ f: C.X_0 \to X \mid f \circ d_{1 0} = 0 \}$$$
Lean4
/-- Morphisms from an `ℕ`-indexed chain complex `C`
to a single object chain complex with `X` concentrated in degree 0
are the same as morphisms `f : C.X 0 ⟶ X` such that `C.d 1 0 ≫ f = 0`.
-/
@[simps apply_coe]
noncomputable def toSingle₀Equiv (C : ChainComplex V ℕ) (X : V) :
(C ⟶ (single₀ V).obj X) ≃ { f : C.X 0 ⟶ X // C.d 1 0 ≫ f = 0 }
where
toFun φ := ⟨φ.f 0, by rw [← φ.comm 1 0, HomologicalComplex.single_obj_d, comp_zero]⟩
invFun
f :=
HomologicalComplex.mkHomToSingle f.1
(fun i hi => by
obtain rfl : i = 1 := by simpa using hi.symm
exact f.2)
left_inv φ := by cat_disch
right_inv f := by simp
