English
Let T be as above; the morphism (H_{n0}(T.mor2)) is mono if and only if δ_T n0 n1 h = 0.
Русский
Пусть T как выше; отображение (H_{n0}(T.mor2)) монообразно тогда и только тогда, когда δ_T n0 n1 h = 0.
LaTeX
$$$$ \operatorname{Mono}\big((H_{n_0} (T.mor_2))\big) \iff \delta_T(n_0,n_1,h) = 0. $$$$
Lean4
/-- The connecting homomorphism
`(singleFunctor C 0).obj S.X₃ ⟶ ((singleFunctor C 0).obj S.X₁)⟦(1 : ℤ)⟧` in the derived
category of `C` when `S` is a short exact short complex in `C`. -/
noncomputable def singleδ : (singleFunctor C 0).obj S.X₃ ⟶ ((singleFunctor C 0).obj S.X₁)⟦(1 : ℤ)⟧ :=
(((SingleFunctors.evaluation _ _ 0).mapIso (singleFunctorsPostcompQIso C)).hom.app S.X₃) ≫
triangleOfSESδ (hS.map_of_exact (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ≫
(((SingleFunctors.evaluation _ _ 0).mapIso (singleFunctorsPostcompQIso C)).inv.app S.X₁)⟦(1 : ℤ)⟧'
