Presentable objects

A functor F : C ⥤ D is κ-accessible (Functor.IsCardinalAccessible) if it commutes with colimits of shape J where J is any κ-filtered category (that is essentially small relative to the universe w such that κ : Cardinal.{w}.). We also introduce another typeclass Functor.IsAccessible saying that there exists a regular cardinal κ such that Functor.IsCardinalAccessible.

An object X of a category is κ-presentable (IsCardinalPresentable) if the functor Hom(X, _) (i.e. coyoneda.obj (op X)) is κ-accessible. Similar as for accessible functors, we define a type class IsAccessible.

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

class CategoryTheory.Functor.IsCardinalAccessible {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop

A functor F : C ⥤ D is κ-accessible (with κ a regular cardinal) if it preserves colimits of shape J where J is any κ-filtered category. In the mathematical literature, some assumptions are often made on the categories C or D (e.g. the existence of κ-filtered colimits, see HasCardinalFilteredColimits below), but here we do not make such assumptions.

• preservesColimitOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : Limits.PreservesColimitsOfShape J F

theorem CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F.IsCardinalAccessible κ] (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : Limits.PreservesColimitsOfShape J F

theorem CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F.IsCardinalAccessible κ] (J : Type u₃) [Category.{v₃, u₃} J] [EssentiallySmall.{w, v₃, u₃} J] [IsCardinalFiltered J κ] : Limits.PreservesColimitsOfShape J F

theorem CategoryTheory.Functor.isCardinalAccessible_of_le {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {κ : Cardinal.{w}} [Fact κ.IsRegular] [F.IsCardinalAccessible κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') : F.IsCardinalAccessible κ'

theorem CategoryTheory.Functor.isCardinalAccessible_of_natIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F.IsCardinalAccessible κ] : G.IsCardinalAccessible κ

class CategoryTheory.Functor.IsAccessible {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

A functor is accessible relative to a universe w if it is κ-accessible for some regular κ : Cardinal.{w}.

• exists_cardinal : ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), F.IsCardinalAccessible κ

theorem CategoryTheory.Functor.isAccessible_of_isCardinalAccessible {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F.IsCardinalAccessible κ] : IsAccessible.{w, v₁, v₂, u₁, u₂} F

@[reducible, inline]

abbrev CategoryTheory.IsCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop

An object X in a category is κ-presentable (for κ a regular cardinal) when the functor Hom(X, _) preserves colimits indexed by κ-filtered categories.

Equations

• CategoryTheory.IsCardinalPresentable X κ = (CategoryTheory.coyoneda.obj (Opposite.op X)).IsCardinalAccessible κ

theorem CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : Limits.PreservesColimitsOfShape J (coyoneda.obj (Opposite.op X))

theorem CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] (J : Type u₃) [Category.{v₃, u₃} J] [EssentiallySmall.{w, v₃, u₃} J] [IsCardinalFiltered J κ] : Limits.PreservesColimitsOfShape J (coyoneda.obj (Opposite.op X))

theorem CategoryTheory.isCardinalPresentable_of_le {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {κ : Cardinal.{w}} [Fact κ.IsRegular] [IsCardinalPresentable X κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') : IsCardinalPresentable X κ'

theorem CategoryTheory.isCardinalPresentable_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] : IsCardinalPresentable Y κ

theorem CategoryTheory.isCardinalPresentable_of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] {C' : Type u₃} [Category.{v₃, u₃} C'] [IsCardinalPresentable X κ] (e : C ≌ C') : IsCardinalPresentable (e.functor.obj X) κ

instance CategoryTheory.isCardinalPresentable_of_isEquivalence {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] {C' : Type u₃} [Category.{v₃, u₃} C'] [IsCardinalPresentable X κ] (F : Functor C C') [F.IsEquivalence] : IsCardinalPresentable (F.obj X) κ

@[simp]

theorem CategoryTheory.isCardinalPresentable_iff_of_isEquivalence {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] {C' : Type u₃} [Category.{v₃, u₃} C'] (F : Functor C C') [F.IsEquivalence] : IsCardinalPresentable (F.obj X) κ ↔ IsCardinalPresentable X κ

@[reducible, inline]

abbrev CategoryTheory.IsPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Prop

An object of a category is presentable relative to a universe w if it is κ-presentable for some regular κ : Cardinal.{w}.

Equations

• CategoryTheory.IsPresentable.{?u.16, ?u.15, ?u.14} X = CategoryTheory.Functor.IsAccessible.{?u.16, ?u.15, ?u.15, ?u.14, ?u.15 + 1} (CategoryTheory.coyoneda.obj (Opposite.op X))

theorem CategoryTheory.isPresentable_of_isCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] : IsPresentable.{w, v₁, u₁} X

class CategoryTheory.HasCardinalFilteredColimits (C : Type u₁) [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop

A category has κ-filtered colimits if it has colimits of shape J for any κ-filtered category J.

• hasColimitsOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : Limits.HasColimitsOfShape J C

instance CategoryTheory.instHasCardinalFilteredColimitsOfHasColimitsOfSize (C : Type u₁) [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.HasColimitsOfSize.{w, w, v₁, u₁} C] : HasCardinalFilteredColimits C κ