theorem homology_les_exact {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {ι : Type u_2} {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : (HomologicalComplex.HomologySequence.composableArrows₅ hS i j hij).Exact

theorem homology_les_naturality {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {ι : Type u_2} {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) : CategoryTheory.CategoryStruct.comp (hS₁.δ i j hij) (HomologicalComplex.homologyMap φ.τ₁ j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₃ i) (hS₂.δ i j hij)

theorem homology_les {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {ι : Type u_2} {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (i j : ι) (hij : c.Rel i j) : (HomologicalComplex.HomologySequence.composableArrows₅ hS₁ i j hij).Exact ∧ CategoryTheory.CategoryStruct.comp (hS₁.δ i j hij) (HomologicalComplex.homologyMap φ.τ₁ j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₃ i) (hS₂.δ i j hij)