Presentable generators

Let C be a category, a regular cardinal κ and P : ObjectProperty C. We define a predicate P.IsCardinalFilteredGenerator κ saying that P consists of κ-presentable objects and that any object in C is a κ-filtered colimit of objects satisfying P. We show that if this condition is satisfied, then P is a strong generator (see IsCardinalFilteredGenerator.isStrongGenerator). Moreover, if C is locally small, we show that any object in C is presentable (see IsCardinalFilteredGenerator.presentable).

Finally, we define a typeclass HasCardinalFilteredGenerator C κ saying that C is locally w-small and that there exists an (essentially) small P such that P.IsCardinalFilteredGenerator κ holds.

References

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

theorem CategoryTheory.Limits.ColimitPresentation.isCardinalPresentable {C : Type u} [Category.{v, u} C] {X : C} {J : Type w} [SmallCategory J] (p : ColimitPresentation J X) (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (j : J), IsCardinalPresentable (p.diag.obj j) κ) [LocallySmall.{w, v, u} C] (κ' : Cardinal.{w}) [Fact κ'.IsRegular] : κ ≤ κ' → ∀ (hJ : HasCardinalLT (Arrow J) κ'), IsCardinalPresentable X κ'

theorem CategoryTheory.ObjectProperty.ColimitOfShape.isCardinalPresentable {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X : C} {J : Type w} [SmallCategory J] (p : P.ColimitOfShape J X) {κ : Cardinal.{w}} [Fact κ.IsRegular] (hP : P ≤ CategoryTheory.isCardinalPresentable C κ) [LocallySmall.{w, v, u} C] (κ' : Cardinal.{w}) [Fact κ'.IsRegular] (h : κ ≤ κ') (hJ : HasCardinalLT (Arrow J) κ') : IsCardinalPresentable X κ'

structure CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop

The condition that P : ObjectProperty C consists of κ-presentable objects and that any object of C is a κ-filtered colimit of objects satisfying P. (This notion is particularly relevant when C is locally w-small and P is essentially w-small, see HasCardinalFilteredGenerators, which appears in the definitions of locally presentable and accessible categories.)

• le_isCardinalPresentable : P ≤ isCardinalPresentable C κ
• exists_colimitsOfShape (X : C) : ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), P.colimitsOfShape J X

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.of_le_isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (h : P.IsCardinalFilteredGenerator κ) {P' : ObjectProperty C} (h₁ : P ≤ P'.isoClosure) (h₂ : P' ≤ isCardinalPresentable C κ) : P'.IsCardinalFilteredGenerator κ

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (h : P.IsCardinalFilteredGenerator κ) : P.isoClosure.IsCardinalFilteredGenerator κ

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isoClosure_iff {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] : P.isoClosure.IsCardinalFilteredGenerator κ ↔ P.IsCardinalFilteredGenerator κ

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.presentable {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (h : P.IsCardinalFilteredGenerator κ) [LocallySmall.{w, v, u} C] (X : C) : IsPresentable.{w, v, u} X

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isStrongGenerator {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (h : P.IsCardinalFilteredGenerator κ) : P.IsStrongGenerator

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isPresentable_eq_retractClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (h : P.IsCardinalFilteredGenerator κ) : isCardinalPresentable C κ = P.retractClosure

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallySmall_isPresentable {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (h : P.IsCardinalFilteredGenerator κ) [ObjectProperty.EssentiallySmall.{w, v, u} P] [LocallySmall.{w, v, u} C] : ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

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

The property that a category C and a regular cardinal κ satisfy P.IsCardinalFilteredGenerators κ for a suitable essentially small P : ObjectProperty C.

• hom_small (X Y : C) : Small.{w, v} (X ⟶ Y)
• exists_generator : ∃ (P : ObjectProperty C) (_ : ObjectProperty.EssentiallySmall.{w, v, u} P), P.IsCardinalFilteredGenerator κ

theorem CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} [ObjectProperty.EssentiallySmall.{w, v, u} P] [LocallySmall.{w, v, u} C] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] (hP : P.IsCardinalFilteredGenerator κ) : HasCardinalFilteredGenerator C κ

theorem CategoryTheory.HasCardinalFilteredGenerator.exists_small_generator (C : Type u) [Category.{v, u} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasCardinalFilteredGenerator C κ] : ∃ (P : ObjectProperty C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ

instance CategoryTheory.instEssentiallySmallIsCardinalPresentableOfHasCardinalFilteredGenerator (C : Type u) [Category.{v, u} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasCardinalFilteredGenerator C κ] : ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)