English
Let T be a distinguished triangle in the derived category of an abelian category C, with integers n0 and n1 such that n0 + 1 = n1. The connecting morphism δ_comp produces a short complex whose three terms are the homology objects H_{n0}(T3), H_{n1}(T1), H_{n1}(T2) and whose two maps are δ and H_{n1}(T1 → T2); this short complex is exact.
Русский
Пусть T — различимая треугольная диаграмма в производной категории abelian C, при этом существуют целые n0, n1 с n0 + 1 = n1. Соединяющее отображение δ_comp образует короткий комплекс между объектами гомологии H_{n0}(T3), H_{n1}(T1), H_{n1}(T2) с картами δ и H_{n1}(T1 → T2); этот короткий комплекс точен.
LaTeX
$$$$ H_{n_0}(T_3) \xrightarrow{\delta_T} H_{n_1}(T_1) \xrightarrow{H_{n_1}(T_1 \to T_2)} H_{n_1}(T_2) \quad\text{is exact} \quad (\operatorname{Im} \delta_T = \ker(H_{n_1}(T_1 \to T_2))). $$$$
Lean4
theorem exact₁ : (ShortComplex.mk _ _ (δ_comp T hT n₀ n₁ h)).Exact :=
(homologyFunctor C 0).homologySequence_exact₁ _ hT _ _ h
