Locally presentable and accessible categories

In this file, we define the notion of locally presentable and accessible categories. We first define these notions for a category C relative to a fixed regular cardinal κ (typeclasses IsCardinalLocallyPresentable C κ and IsCardinalAccessibleCategory C κ). The existence of such a regular cardinal κ is asserted in the typeclasses IsLocallyPresentable and IsAccessibleCategory. We show that in a locally presentable or accessible category, any object is presentable.

References

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

class CategoryTheory.IsCardinalLocallyPresentable (C : Type u) [Category.{v, u} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] extends CategoryTheory.HasCardinalFilteredGenerator C κ, CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C : Prop

Given a regular cardinal κ, a category C is κ-locally presentable if it is cocomplete and admits a (small) family G : ι → C of κ-presentable objects such that any object identifies as a κ-filtered colimit of these objects.

• hom_small (X Y : C) : Small.{w, v} (X ⟶ Y)
• exists_generator : ∃ (P : ObjectProperty C) (_ : ObjectProperty.EssentiallySmall.{w, v, u} P), P.IsCardinalFilteredGenerator κ
• has_colimits_of_shape (J : Type w) [Category.{w, w} J] : HasColimitsOfShape J C

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

Given a regular cardinal κ, a category C is κ-accessible if it has κ-filtered colimits and admits a (small) family G : ι → C of κ-presentable objects such that any object identifies as a κ-filtered colimit of these objects.

• hom_small (X Y : C) : Small.{w, v} (X ⟶ Y)
• exists_generator : ∃ (P : ObjectProperty C) (_ : ObjectProperty.EssentiallySmall.{w, v, u} P), P.IsCardinalFilteredGenerator κ
• hasColimitsOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : Limits.HasColimitsOfShape J C

instance CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable (C : Type u) [Category.{v, u} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalLocallyPresentable C κ] : IsCardinalAccessibleCategory C κ

@[reducible, inline]

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

A category is locally finitely presentable if it is locally ℵ₀-presentable.

Equations

• CategoryTheory.IsLocallyFinitelyPresentable C = CategoryTheory.IsCardinalLocallyPresentable C Cardinal.aleph0

@[reducible, inline]

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

A category is finitely accessible if it is ℵ₀-accessible.

Equations

• CategoryTheory.IsFinitelyAccessibleCategory C = CategoryTheory.IsCardinalAccessibleCategory C Cardinal.aleph0

class CategoryTheory.IsLocallyPresentable (C : Type u) [hC : Category.{v, u} C] : Prop

A category C is locally presentable if it is κ-locally presentable for some regular cardinal κ.

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

class CategoryTheory.IsAccessibleCategory (C : Type u) [hC : Category.{v, u} C] : Prop

A category C is accessible if it is κ-accessible for some regular cardinal κ.

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

instance CategoryTheory.instIsAccessibleCategoryOfIsLocallyPresentable (C : Type u) [hC : Category.{v, u} C] [IsLocallyPresentable.{w, v, u} C] : IsAccessibleCategory.{w, v, u} C

instance CategoryTheory.instIsPresentableOfIsAccessibleCategory (C : Type u) [hC : Category.{v, u} C] [IsAccessibleCategory.{w, v, u} C] (X : C) : IsPresentable.{w, v, u} X