English
The forgetful functor forget V G preserves colimits of shape J as soon as forgetful postcomposition preserves them.
Русский
Забывающий функтор forget V G сохраняет колимиты формы J, если после композиции с забыванием сохраняются колимиты.
LaTeX
$$$\operatorname{PreservesColimitsOfShape}(J, \mathrm{forget}(V,G)).$$$
Lean4
/-- `Action.forget V G : Action V G ⥤ V` preserves the colimit of some `K : J ⥤ Action V G` if
`K ⋙ Action.forget V G` has a colimit. -/
noncomputable instance {J : Type*} [Category J] (K : J ⥤ Action V G) [HasColimit (K ⋙ forget V G)] :
PreservesColimit K (Action.forget V G) :=
by
change
PreservesColimit K
((Action.functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
have (k : SingleObj G) : HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
inferInstanceAs (HasColimit (K ⋙ forget V G))
infer_instance
