English
If K : J ⥤ C and F : C ⥤ Action V G, then PreservesColimit K (F ⋙ forget V G) implies PreservesColimit K F.
Русский
Если K : J ⥤ C и F : C ⥤ Action V G, то сохранение колимита после забывания влечет сохранение колимита самим F.
LaTeX
$$$\operatorname{PreservesColimit}(K, F) \Leftarrow \operatorname{PreservesColimit}(K, F \circ \mathrm{forget}).$$$
Lean4
/-- `F : C ⥤ Action V G` preserves the colimit of some `K : J ⥤ C` if
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
theorem preservesColimit_of_preserves (F : C ⥤ Action V G) {J : Type*} [Category J] (K : J ⥤ C)
(h : PreservesColimit K (F ⋙ Action.forget V G)) : PreservesColimit K F :=
by
let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor
have : PreservesColimit K F' := SingleObj.preservesColimit _ _ h
apply preservesColimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor
