commShiftOfLocalization_iso_inv_app

English

As in 79235, the induced shiftIso hom component factors through e' and G-shift pieces.

Русский

Как и в пункте 79235, гомоморфизм индуцированного сдвигового изоморфизма делится через части e' и G-сдвига.

LaTeX

$$$ (\text{induced}_{}\text{shiftIso}_{}(L,G,M,F',e')\ n\ a\ a'\ ha').hom.app (L.obj X) = (F' 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 commShiftOfLocalization_iso_inv_app (a : A) (X : C) :
    letI := Functor.commShiftOfLocalization L W A F F'
    (F'.commShiftIso a).inv.app (L.obj X) =
      (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
        (F.commShiftIso a).inv.app X ≫ (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫ F'.map ((L.commShiftIso a).hom.app X) :=
  by apply commShiftOfLocalization.iso_inv_app

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