Properties of objects on preadditive categories equipped with shift #
In this file, we show that if C is a preadditive category
equipped with a shift by an additive monoid A, and
P : ObjectProperty C is stable under the shift,
then the shift functors on the full subcategory associated
to P are additive if the shift functors on C are.
This instance is put in a separate file in order to reduce imports.
instance
CategoryTheory.ObjectProperty.instAdditiveFullSubcategoryShiftFunctor
{C : Type u_1}
[Category.{v_1, u_1} C]
(P : ObjectProperty C)
{A : Type u_2}
[AddMonoid A]
[HasShift C A]
[P.IsStableUnderShift A]
[Preadditive C]
(n : A)
[(shiftFunctor C n).Additive]
: