English
For f: X ⟶ Y⟦n⟧, the induced shift map equals the conjugation by e' and G-shift, i.e., F.shiftMap equals e' a, G.shiftMap, and e' a' inverses composed with L.map f.
Русский
Для f: X ⟶ Y⟦n⟧ индуцированная карта сдвига равна конъюгации через e', сдвиг G и обратные стороны e' a, e' a'.
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
@[reassoc]
theorem induced_shiftMap {n : M} {X Y : C} (f : X ⟶ Y⟦n⟧) (a a' : M) (h : n + a = a') :
letI := induced e M F' e'
F.shiftMap (L.map f ≫ (L.commShiftIso n).hom.app _) a a' h =
(e' a).hom.app X ≫ G.shiftMap f a a' h ≫ (e' a').inv.app Y :=
by
dsimp [shiftMap]
rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc]
nth_rw 2 [← Functor.map_comp_assoc]
simp only [comp_obj, Iso.hom_inv_id_app, map_id, id_comp]
rw [← NatTrans.naturality_assoc]
rfl
