English
If C is locally w-small and Y: K ⥤ C has a colimit cocone c, and κ is regular with suitable hypotheses, then the apex c.pt is κ-presentable whenever each Y.obj k is κ-presentable.
Русский
Пусть C локально w-малка и имеется колимит кокон c над Y: K ⥤ C; при регулярном κ и прочих условиях вершина колимита κ-представляема тогда, когда каждый Y.obj k κ-представляема.
LaTeX
$$$\text{IsCardinalPresentable}(c.pt,\kappa)$$$
Lean4
theorem isCardinalAccessible_of_isLimit {K : Type u'} [Category.{v'} K] {F : K ⥤ C ⥤ Type w'} (c : Cone F)
(hc : IsLimit c) (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasLimitsOfShape K (Type w')]
(hK : HasCardinalLT (Arrow K) κ) [∀ k, (F.obj k).IsCardinalAccessible κ] : c.pt.IsCardinalAccessible κ where
preservesColimitOfShape
{J _
_} :=
⟨fun {X} ↦
⟨fun {cX} hcX ↦ by
have := fun k ↦ preservesColimitsOfShape_of_isCardinalAccessible (F.obj k) κ J
exact
⟨Accessible.Limits.isColimitMapCocone c (fun Y ↦ isLimitOfPreserves ((evaluation C (Type w')).obj Y) hc) κ hK
cX (fun k ↦ isColimitOfPreserves (F.obj k) hcX)⟩⟩⟩
