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 κ

instance CategoryTheory.Functor.instIsCardinalAccessibleId {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : (Functor.id C).IsCardinalAccessible κ

instance CategoryTheory.Functor.instIsCardinalAccessibleComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (κ : Cardinal.{w}) [Fact κ.IsRegular] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.IsCardinalAccessible κ] [G.IsCardinalAccessible κ] : (F.comp G).IsCardinalAccessible κ

instance CategoryTheory.Functor.instIsCardinalAccessibleOfPreservesColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.PreservesColimitsOfSize.{w, w, v₁, v₂, u₁, u₂} F] : F.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 κ

def CategoryTheory.isCardinalPresentable (C : Type u₁) [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : ObjectProperty C

The property of objects that are κ-presentable.

Equations

• CategoryTheory.isCardinalPresentable C κ X = CategoryTheory.IsCardinalPresentable X κ

instance CategoryTheory.instIsCardinalPresentableObjIsCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : (isCardinalPresentable C κ).FullSubcategory) : IsCardinalPresentable X.obj κ

instance CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : (isCardinalPresentable C κ).FullSubcategory) : IsCardinalPresentable ((isCardinalPresentable C κ).ι.obj X) κ

theorem CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] : IsCardinalPresentable X κ ↔ (coyoneda.obj (Opposite.op X)).IsCardinalAccessible κ

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

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_monotone (C : Type u₁) [Category.{v₁, u₁} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') : isCardinalPresentable C κ ≤ isCardinalPresentable C κ'

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 κ

instance CategoryTheory.instIsClosedUnderIsomorphismsIsCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms

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 κ

theorem CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit {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 κ] {F : Functor J C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) (f : X ⟶ c.pt) : ∃ (j : J) (f' : X ⟶ F.obj j), CategoryStruct.comp f' (c.ι.app j) = f

theorem CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit {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 κ] {F : Functor J C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) {i₁ i₂ : J} (f₁ : X ⟶ F.obj i₁) (f₂ : X ⟶ F.obj i₂) (hf : CategoryStruct.comp f₁ (c.ι.app i₁) = CategoryStruct.comp f₂ (c.ι.app i₂)) : ∃ (j : J) (u : i₁ ⟶ j) (v : i₂ ⟶ j), CategoryStruct.comp f₁ (F.map u) = CategoryStruct.comp f₂ (F.map v)

theorem CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit' {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 κ] {F : Functor J C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) {i : J} (f₁ f₂ : X ⟶ F.obj i) (hf : CategoryStruct.comp f₁ (c.ι.app i) = CategoryStruct.comp f₂ (c.ι.app i)) : ∃ (j : J) (u : i ⟶ j), CategoryStruct.comp f₁ (F.map u) = CategoryStruct.comp f₂ (F.map u)

theorem CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] : IsCardinalPresentable X κ ↔ (uliftCoyoneda.{t, v₁, u₁}.obj (Opposite.op X)).IsCardinalAccessible κ

instance CategoryTheory.instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] : (uliftCoyoneda.{t, v₁, u₁}.obj (Opposite.op X)).IsCardinalAccessible κ

@[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 κ