Localization of the linearity of the shift functors

If L : C ⥤ D is a localization functor with respect to W : MorphismProperty C and both C and D have been equipped with R-linear category structures such that L is R-linear and the shift functors on C are R-linear, then the shift functors on D are R-linear.

theorem CategoryTheory.Shift.linear_of_localization (R : Type u_1) [Ring R] {C : Type u_4} [Category.{v_1, u_4} C] [Preadditive C] [Linear R C] {D : Type u_2} [Category.{v_2, u_2} D] [Preadditive D] [Linear R D] {M : Type u_3} [AddMonoid M] [HasShift C M] [∀ (n : M), Functor.Linear R (shiftFunctor C n)] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [Functor.Linear R L] [HasShift D M] [L.CommShift M] (n : M) : Functor.Linear R (shiftFunctor D n)

instance CategoryTheory.Shift.instLinearLocalizationShiftFunctorOfCommShiftOfQ (R : Type u_1) [Ring R] {C : Type u_4} [Category.{v_1, u_4} C] [Preadditive C] [Linear R C] {M : Type u_3} [AddMonoid M] [HasShift C M] [∀ (n : M), Functor.Linear R (shiftFunctor C n)] (W : MorphismProperty C) [HasShift W.Localization M] [W.Q.CommShift M] [Preadditive W.Localization] [Linear R W.Localization] [Functor.Linear R W.Q] (n : M) : Functor.Linear R (shiftFunctor W.Localization n)

instance CategoryTheory.Shift.instLinearLocalization'ShiftFunctorOfCommShiftOfQ' (R : Type u_1) [Ring R] {C : Type u_5} [Category.{v_1, u_5} C] [Preadditive C] [Linear R C] {M : Type u_3} [AddMonoid M] [HasShift C M] [∀ (n : M), Functor.Linear R (shiftFunctor C n)] (W : MorphismProperty C) (n : M) [W.HasLocalization] [HasShift W.Localization' M] [W.Q'.CommShift M] [Preadditive W.Localization'] [Linear R W.Localization'] [Functor.Linear R W.Q'] : Functor.Linear R (shiftFunctor W.Localization' n)