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] : (shiftFunctor P.FullSubcategory n).Additive