English
Alternative formalization: PreservesColimitsOfSize (F) if PreservesColimitsOfSize (F ⋙ forget).
Русский
Альтернативная формализация: сохранение колимитов по размеру, если после забывания сохраняются колимиты по размеру.
LaTeX
$$$\operatorname{PreservesColimitsOfSize}(F) \Leftarrow \operatorname{PreservesColimitsOfSize}(F \circ \mathrm{forget}).$$$
Lean4
/-- `Action.forget V G : Action V G ⥤ V` preserves the limit of some `K : J ⥤ Action V G` if
`K ⋙ Action.forget V G` has a limit. -/
noncomputable instance {J : Type*} [Category J] (K : J ⥤ Action V G) [HasLimit (K ⋙ forget V G)] :
PreservesLimit K (Action.forget V G) :=
by
change
PreservesLimit K
((Action.functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
have (k : SingleObj G) : HasLimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
inferInstanceAs (HasLimit (K ⋙ forget V G))
infer_instance
