English
Relates the hom-component of a shift isomorphism against a shifted map, showing equality of two routes from (F.shift a).obj X to (F.shift a'').obj Y via the intermediate object (F.shift a').obj Y.
Русский
Связывает гом-компонент изоморфизма сдвига с отображением, показывая равенство двух путей между объектами shifting.
LaTeX
$$$(F.shiftIso mn a a'' (by rw [\lt- hnm, \lt- ha'', \lt- ha', add_assoc])).hom.app X = (shift F a).map ((shiftFunctorAdd' C m n mn hnm).hom.app X) ≫ (shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (shiftIso F m a' a'' ha'').hom.app X$$$
Lean4
/-- When `f : X ⟶ Y⟦m⟧`, `m + n = mn`, `n + a = a'` and `ha'' : m + a' = a''`, this lemma
relates the two morphisms `F.shiftMap f a' a'' ha''` and `(F.shift a).map (f⟦n⟧')`. Indeed,
via canonical isomorphisms, they both identity to morphisms
`(F.shift a').obj X ⟶ (F.shift a'').obj Y`.
-/
theorem shiftIso_hom_app_comp_shiftMap {X Y : C} {m : M} (f : X ⟶ Y⟦m⟧) (n mn : M) (hnm : m + n = mn) (a a' a'' : M)
(ha' : n + a = a') (ha'' : m + a' = a'') :
(F.shiftIso n a a' ha').hom.app X ≫ F.shiftMap f a' a'' ha'' =
(F.shift a).map (f⟦n⟧') ≫
(F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app Y) ≫
(F.shiftIso mn a a'' (by rw [← ha'', ← ha', ← hnm, add_assoc])).hom.app Y :=
by
simp only [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'' Y, ← Functor.map_comp_assoc, Iso.inv_hom_id_app,
Functor.map_id, id_comp, comp_obj, shiftIso_hom_naturality_assoc, shiftMap]
