preservesLimitsOfShape_of_preserves

English

If F preserves limits of shape J after forgetful postcomposition, then F preserves limits of shape J.

Русский

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

LaTeX

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

Lean4

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

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