English
As in 79236, shift maps compose via e' and the G-shift map, reflecting a conjugation by e'.
Русский
Как и в 79236, отображения сдвига соединяются через e' и отображение сдвига G, выражая конъюгацию через e'.
LaTeX
$$$ F.shiftMap (L.map f \gg (L.commShiftIso n).hom.app _) a a' h = (e' a).hom.app X \gg G.shiftMap f a a' h \gg (e' a').inv.app Y $$$
Lean4
instance commShift_iso_hom_of_localization :
letI := Functor.commShiftOfLocalization L W A F F'
NatTrans.CommShift (Lifting.iso L W F F').hom A :=
by
letI := Functor.commShiftOfLocalization L W A F F'
constructor
intro a
ext X
simp only [comp_app, Functor.whiskerRight_app, Functor.whiskerLeft_app, Functor.commShiftIso_comp_hom_app,
Functor.commShiftOfLocalization_iso_hom_app, Category.assoc, ← Functor.map_comp, ← Functor.map_comp_assoc,
Iso.hom_inv_id_app, Functor.map_id, Iso.inv_hom_id_app, Category.comp_id, Category.id_comp, Functor.comp_obj]
