instLinearLocalization'ShiftFunctorOfCommShiftOfQ'

English

If L is a localization with respect to W and is R-linear, and D has a shift by M with CommShift, then the shift functor on D by any n∈M is R-linear.

Русский

Если L является локализацией по отношению к W и R-линейна, и у D есть сдвиг на M с CommShift, тогда сдвиговая на D по любому n∈M является R-линейной.

LaTeX

$$$ [L.IsLocalization\ W]\ [L.Linear\ R]\ [HasShift\ D\ M]\ [L.CommShift\ M]\ (n\in M)\;\Rightarrow\; (shiftFunctor\ D\ n).Linear\ R $$$

Lean4

instance (n : M) [W.HasLocalization] [HasShift W.Localization' M] [W.Q'.CommShift M] [Preadditive W.Localization']
    [Linear R W.Localization'] [W.Q'.Linear R] : (shiftFunctor W.Localization' n).Linear R :=
  linear_of_localization _ W.Q' W _

Похожие утверждения