English
For shifted morphisms f,g with a, b, c degrees and a functor F, the map of the composite f.comp g along h equals the composite of the maps, i.e., (f.comp g h).map F = (f.map F).comp (g.map F) h.
Русский
Для сдвинутых морфизмов f,g с степенями a,b и с функтором F выполняется: (f.comp g h).map F = (f.map F).comp (g.map F) h.
LaTeX
$$$ (f.comp g h).map F = (f.map F).comp (g.map F) h $$$
Lean4
theorem map_comp {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b) (h : b + a = c) (F : C ⥤ D) [F.CommShift M] :
(f.comp g h).map F = (f.map F).comp (g.map F) h :=
by
dsimp [comp, map]
simp only [Functor.map_comp, assoc]
erw [← NatTrans.naturality_assoc]
simp only [Functor.comp_map, F.commShiftIso_add' h, Functor.CommShift.isoAdd'_hom_app, ← Functor.map_comp_assoc,
Iso.inv_hom_id_app, Functor.comp_obj, comp_id]
