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

## Equations

- ⋯ = ⋯