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
- ⋯ = ⋯