English
For F: J ⥤ C, E : K ⥤ J, G : C ⥤ D with needed colimits, the canonical compatibility holds: colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G.
Русский
Для F : J ⥤ C, E : K ⥤ J, G : C ⥤ D при существовании колимитов имеем совместимость: colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G.
LaTeX
$$$ \\operatorname{colimit.post} (E \\cdot F) G \\; \\circ \\; G.map (\\operatorname{colimit.pre} F E) = \\operatorname{colimit.pre} (F \\cdot G) E \\; \\circ \\ \\operatorname{colimit.post} F G $$$
Lean4
theorem pre_map [HasColimitsOfShape K C] (E : K ⥤ J) :
colimit.pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ colimit.pre G E :=
by
ext
rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]
rfl
