Locally presentable categories and strong generators

In this file, we show that a category is locally κ-presentable iff it is cocomplete and has a strong generator consisting of κ-presentable objects. This is theorem 1.20 in the book by Adámek and Rosický.

In particular, if a category is locally κ-presentable, it is also locally κ'-presentable for any regular cardinal κ' such that κ ≤ κ'.

References

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

theorem CategoryTheory.IsCardinalFilteredGenerator.of_isDense {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {J : Type u'} [Category.{v', u'} J] [EssentiallySmall.{w, v', u'} J] (F : Functor J C) [F.IsDense] (κ : Cardinal.{w}) [Fact κ.IsRegular] [∀ (j : J), IsCardinalPresentable (F.obj j) κ] [∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ] : (⊤.map F).IsCardinalFilteredGenerator κ

theorem CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w, v, u} P] (κ : Cardinal.{w}) [Fact κ.IsRegular] [P.ι.IsDense] [LocallySmall.{w, v, u} C] (hP : P ≤ isCardinalPresentable C κ) [∀ (X : C), IsCardinalFiltered (CostructuredArrow P.ι X) κ] : P.IsCardinalFilteredGenerator κ

instance CategoryTheory.ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.HasColimitsOfSize.{w, w, v, u} C] (X : C) : IsCardinalFiltered (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) κ

instance CategoryTheory.ObjectProperty.isFiltered_costructuredArrow_colimitsCardinalClosure_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.HasColimitsOfSize.{w, w, v, u} C] (X : C) : IsFiltered (CostructuredArrow (P.colimitsCardinalClosure κ).ι X)

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι {C : Type u} [Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [Limits.HasColimitsOfSize.{w, w, v, u} C] [LocallySmall.{w, v, u} C] {P : ObjectProperty C} [ObjectProperty.Small.{w, v, u} P] (hS₁ : P.IsStrongGenerator) (hS₂ : P ≤ isCardinalPresentable C κ) : (P.colimitsCardinalClosure κ).ι.IsDense

theorem CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable {C : Type u} [Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [LocallySmall.{w, v, u} C] (P : ObjectProperty C) (hP : P ≤ isCardinalPresentable C κ) : P.colimitsCardinalClosure κ ≤ isCardinalPresentable C κ

theorem CategoryTheory.IsStrongGenerator.colimitsCardinalClosure_eq_isCardinalPresentable {C : Type u} [Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [Limits.HasColimitsOfSize.{w, w, v, u} C] [LocallySmall.{w, v, u} C] {P : ObjectProperty C} [ObjectProperty.Small.{w, v, u} P] (hS₁ : P.IsStrongGenerator) (hS₂ : P ≤ isCardinalPresentable C κ) : isCardinalPresentable C κ = P.colimitsCardinalClosure κ

theorem CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator (C : Type u) [Category.{v, u} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.HasColimitsOfSize.{w, w, v, u} C] [LocallySmall.{w, v, u} C] : IsCardinalLocallyPresentable C κ ↔ ∃ (P : ObjectProperty C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

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