English
If the diagram Y: K ⥤ C is locally small and every object Y.obj k is κ-presentable, then the apex of any colimit cocone c: Cocone Y is κ-presentable provided κ is regular and K has limits of shape as required.
Русский
Пусть диаграмма Y: K ⥤ C локально мала, и каждый объект Y.obj k κ-представим; тогда вершина колимита кокона c над Y κ-представляема при регулярном κ и наличии нужных пределов формы Kᵒᵖ.
LaTeX
$$$\text{IsCardinalPresentable}(c.pt, κ)$$$
Lean4
/-- In case `C` is locally `w`-small, use `isCardinalPresentable_of_isColimit`. -/
theorem isCardinalPresentable_of_isColimit' {K : Type u'} [Category.{v'} K] {Y : K ⥤ C} (c : Cocone Y)
(hc : IsColimit c) (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasLimitsOfShape Kᵒᵖ (Type v)]
(hK : HasCardinalLT (Arrow K) κ) [∀ k, IsCardinalPresentable (Y.obj k) κ] : IsCardinalPresentable c.pt κ :=
by
have (k : Kᵒᵖ) : ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ := by dsimp; infer_instance
exact Functor.isCardinalAccessible_of_isLimit (coyoneda.mapCone c.op) (isLimitOfPreserves _ hc.op) κ (by simpa)
