κ-presentable objects form a dense subcategory

In a κ-accessible category C, the inclusion of the full subcategory of κ-presentable objects is a dense functor. This expresses canonically any object X : C as a colimit of κ-presentable objects, and we show that this is a κ-filtered colimit.

theorem CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentable (C : Type u) [Category.{v, u} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] : (isCardinalPresentable C κ).IsCardinalFilteredGenerator κ

instance CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow {C : Type u} [Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] {J : Type u'} [Category.{v', u'} J] [EssentiallySmall.{w, v', u'} J] [IsCardinalFiltered J κ] {X : C} (p : (isCardinalPresentable C κ).ColimitOfShape J X) : p.toCostructuredArrow.Final

instance CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι {C : Type u} [Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] : (isCardinalPresentable C κ).ι.IsDense

instance CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι {C : Type u} [Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] (X : C) : IsCardinalFiltered (CostructuredArrow (isCardinalPresentable C κ).ι X) κ

instance CategoryTheory.IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι {C : Type u} [Category.{v, u} C] [IsFinitelyAccessibleCategory C] (X : C) : IsFiltered (CostructuredArrow (ObjectProperty.isFinitelyPresentable C).ι X)

instance CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι {C : Type u} [Category.{v, u} C] [IsFinitelyAccessibleCategory C] : (ObjectProperty.isFinitelyPresentable C).ι.IsDense

instance CategoryTheory.IsFinitelyAccessibleCategory.instEssentiallySmallIsFinitelyPresentable {C : Type u} [Category.{v, u} C] [IsFinitelyAccessibleCategory C] : ObjectProperty.EssentiallySmall.{w, v, u} (ObjectProperty.isFinitelyPresentable C)