preservesLimitsOfSize_of_preserves

English

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

Русский

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

LaTeX

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

Lean4

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

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