English
If C is locally small and has limits of shape Kᵒᵖ, and Y: K ⥤ C has a cocone c which is a colimit, then c.pt is κ-presentable whenever each Y.obj k is κ-presentable, under regular κ.
Русский
Пусть C локально мала и имеет пределы формы Kᵒᵖ; кокон Y: K ⥤ C имеет колимит; вершина c.pt κ-представляема при регулярном κ, если каждый Y.obj k κ-представим.
LaTeX
$$$\text{IsCardinalPresentable}(c.pt, κ)$$$
Lean4
theorem isCardinalPresentable_of_isColimit [LocallySmall.{w} C] {K : Type u'} [Category.{v'} K]
[HasLimitsOfShape Kᵒᵖ (Type w)] {Y : K ⥤ C} (c : Cocone Y) (hc : IsColimit c) (κ : Cardinal.{w}) [Fact κ.IsRegular]
(hK : HasCardinalLT (Arrow K) κ) [∀ k, IsCardinalPresentable (Y.obj k) κ] : IsCardinalPresentable c.pt κ :=
by
let e := ShrinkHoms.equivalence.{w} C
have (k : K) : IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ := by dsimp; infer_instance
rw [← isCardinalPresentable_iff_of_isEquivalence c.pt κ e.functor]
exact isCardinalPresentable_of_isColimit' _ (isColimitOfPreserves e.functor hc) κ hK
