The homological functor

In this file, it is shown that if C is an abelian category, then homologyFunctor C (ComplexShape.up ℤ) n is a homological functor HomotopyCategory C (ComplexShape.up ℤ) ⥤ C. As distinguished triangles in the homotopy category can be characterized in terms of degreewise split short exact sequences of cochain complexes, this follows from the homology sequence of a short exact sequences of homological complexes.

instance HomotopyCategory.instIsHomologicalIntUpHomologyFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (n : ℤ) : (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).IsHomological