English
For functors E : K ⥤ J, F : J ⥤ C, G : C ⥤ D, if all required colimits exist, then the two ways of composing post and pre maps are equal: colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G.
Русский
Пусть E : K ⥤ J, F : J ⥤ C, G : C ⥤ D существуют необходимые колимиты; тогда совпадают два способа композиции post и pre: 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
/-- If a `E ⋙ F` has a colimit, and `E` is an equivalence, we can construct a colimit of `F`.
-/
theorem hasColimit_of_equivalence_comp (e : K ≌ J) [HasColimit (e.functor ⋙ F)] : HasColimit F :=
by
haveI : HasColimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasColimit_equivalence_comp e.symm
apply hasColimit_of_iso (e.invFunIdAssoc F).symm
