preservesColimitsOfShape_of_isCardinalPresentable

English

If X is κ-presentable, then the coyoneda construction Coyoneda.obj (op X) preserves colimits of shape J whenever J is small.

Русский

Если X является κ-представляющим, то Coyoneda.obj (op X) сохраняет колимиты по форме J для малых J.

LaTeX

$$$[IsCardinalPresentable X \kappa] \Rightarrow \text{PreservesColimitsOfShape } J (\text{coyoneda.obj } (op X))$$$

Lean4

theorem preservesColimitsOfShape_of_isCardinalPresentable [IsCardinalPresentable X κ] (J : Type w) [SmallCategory.{w} J]
    [IsCardinalFiltered J κ] : PreservesColimitsOfShape J (coyoneda.obj (op X)) :=
  (coyoneda.obj (op X)).preservesColimitsOfShape_of_isCardinalAccessible κ J

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