linear_of_localization — Mathlib

English

Similar to item 79235, but with general n, a, a' and the induced shiftIso homogeneous decomposition formula.

Русский

Аналогично пункту 79235, но для произвольных n, a, a' и индуцированного разложения гомоморфизма ShiftIso.

LaTeX

$$$ (\text{induced}_{{e,M,F',e'}}.\text{shiftIso})\hom.app (L.obj X) = (F'.shift a).map ((L.commShiftIso n).inv.app X) \gg (e' a).hom.app (X⟦n⟧) \gg (G.shiftIso n a a' ha').hom.app X \gg (e' a').inv.app X $$$

Lean4

theorem linear_of_localization [L.IsLocalization W] [L.Linear R] [HasShift D M] [L.CommShift M] (n : M) :
    (shiftFunctor D n).Linear R :=
  by
  have : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n) := ⟨(L.commShiftIso n).symm⟩
  rw [← Localization.functor_linear_iff L W R (shiftFunctor C n ⋙ L) (shiftFunctor D n)]
  infer_instance

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