instAdditiveLocalizationShiftFunctorInt

English

The shift functor on localization by an integer index n is additive, i.e., it preserves addition of morphisms.

Русский

Сдвиговый функтор на локализации по целому индексу n сохраняет сложение морфизмов.

LaTeX

$$$\forall n\in\mathbb{Z},\; (\text{shiftFunctor } W.Localization\; n)\;\text{Additive}$$$

Lean4

instance (n : ℤ) : (shiftFunctor (W.Localization) n).Additive :=
  by
  rw [Localization.functor_additive_iff W.Q W]
  exact Functor.additive_of_iso (W.Q.commShiftIso n)

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