κ-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 κ]
:
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)
:
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) κ