English
In a category with shifts, the operation map respects composition of shifted morphisms under opposite shifts. More precisely, for any f : ShiftedHom X Y a and F, G functors with commutative shift structure, map respects composition: f.map (F ⋙ G) = (f.map F).map G.
Русский
В категории с сдвигами операция отображения сохраняет композицию ShiftedHom: для f : ShiftedHom X Y a и функций F,G с совместным сдвигом выполняется f.map(F ⋙ G) = (f.map F).map G.
LaTeX
$$$\\forall a\\, (f:\\\u2060ShiftedHom\\ X\\ Y\\ a)\\, (F:C\\to D)\\, (G:D\\to E),\\ F.CommShift\\ u\\, G.CommShift\\ u,\\ (f.map(F \\circ G)) = (f.map F).map G.$$$
Lean4
theorem comp_map {a : M} (f : ShiftedHom X Y a) (F : C ⥤ D) [F.CommShift M] (G : D ⥤ E) [G.CommShift M] :
f.map (F ⋙ G) = (f.map F).map G := by simp [map, Functor.commShiftIso_comp_hom_app]
