preservesColimitsOfSize_of_preserves

English

If F preserves colimits of a given size after forgetting, then F preserves colimits of that size.

Русский

Если F сохраняет колимиты заданного размера после забывания, то F сохраняет колимиты этого размера.

LaTeX

$$$\operatorname{PreservesColimitsOfSize}(F) \Leftarrow \operatorname{PreservesColimitsOfSize}(F \circ \mathrm{forget}).$$$

Lean4

/-- `F : C ⥤ Action V G` preserves colimits of some size
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
theorem preservesColimitsOfSize_of_preserves (F : C ⥤ Action V G)
    (h : PreservesColimitsOfSize.{w₂, w₁} (F ⋙ Action.forget V G)) : PreservesColimitsOfSize.{w₂, w₁} F :=
  by
  constructor
  intro J _
  apply Action.preservesColimitsOfShape_of_preserves
  exact PreservesColimitsOfSize.preservesColimitsOfShape

Похожие утверждения