The projections of short complexes are additive #
In a preadditive category, the three projections ShortComplex.π₁, ShortComplex.π₂ and
ShortComplex.π₃ from short complexes to their terms are additive functors, because morphisms of
short complexes are added componentwise. In particular each component of a finite sum of
morphisms of short complexes is the sum of the components (CategoryTheory.Functor.map_sum).
instance
CategoryTheory.ShortComplex.additive_π₁
{C : Type u_1}
[Category.{v_1, u_1} C]
[Preadditive C]
:
instance
CategoryTheory.ShortComplex.additive_π₂
{C : Type u_1}
[Category.{v_1, u_1} C]
[Preadditive C]
:
instance
CategoryTheory.ShortComplex.additive_π₃
{C : Type u_1}
[Category.{v_1, u_1} C]
[Preadditive C]
: