Homotopy equivalences between chain complexes

If 0 ⟶ K₁ ⟶ K₂ ⟶ K₃ ⟶ 0 is a degreewise short exact sequence of chain complexes, we show that K₁ ⟶ K₂ is a homotopy equivalence iff K₃ is contractible, and K₂ ⟶ K₃ is a homotopy equivalence iff K₁.

theorem ChainComplex.homotopyEquivalences_shortComplexF_iff_of_degreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (S : CategoryTheory.ShortComplex (ChainComplex C ℕ)) (σ : (n : ℕ) → (S.map (HomologicalComplex.eval C (ComplexShape.down ℕ) n)).Splitting) : HomologicalComplex.homotopyEquivalences C (ComplexShape.down ℕ) S.f ↔ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id S.X₃) 0)

theorem ChainComplex.homotopyEquivalences_shortComplexG_iff_of_degreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (S : CategoryTheory.ShortComplex (ChainComplex C ℕ)) (σ : (n : ℕ) → (S.map (HomologicalComplex.eval C (ComplexShape.down ℕ) n)).Splitting) : HomologicalComplex.homotopyEquivalences C (ComplexShape.down ℕ) S.g ↔ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id S.X₁) 0)