preservesColimitsOfShape_of_preserves

English

If F preserves colimits of shape J after forgetting, then F preserves colimits of shape J.

Русский

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

LaTeX

$$$\operatorname{PreservesColimitsOfShape}(J, F) \Leftarrow \operatorname{PreservesColimitsOfShape}(J, F \circ \mathrm{forget}).$$$

Lean4

/-- `F : C ⥤ Action V G` preserves colimits of some shape `J`
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
theorem preservesColimitsOfShape_of_preserves (F : C ⥤ Action V G) {J : Type*} [Category J]
    (h : PreservesColimitsOfShape J (F ⋙ Action.forget V G)) : PreservesColimitsOfShape J F :=
  by
  constructor
  intro K
  apply Action.preservesColimit_of_preserves
  exact PreservesColimitsOfShape.preservesColimit

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