English
If F : C ⥤ Action V G preserves limits whenever F ⋙ forget V G does, then F preserves limits.
Русский
Если F сохраняет пределы тогда и только тогда, когда F ⋙ forget сохраняет пределы, то F сохраняет пределы.
LaTeX
$$$\operatorname{PreservesLimit}(K, F) \leftarrow \operatorname{PreservesLimit}(K, F \circ \mathrm{forget}).$$$
Lean4
/-- `F : C ⥤ Action V G` preserves the limit of some `K : J ⥤ C` if
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
theorem preservesLimit_of_preserves (F : C ⥤ Action V G) {J : Type*} [Category J] (K : J ⥤ C)
(h : PreservesLimit K (F ⋙ Action.forget V G)) : PreservesLimit K F :=
by
let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor
have : PreservesLimit K F' := SingleObj.preservesLimit _ _ h
apply preservesLimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor
