Presentable objects and adjunctions #
If adj : F ⊣ G and G is κ-accessible for a regular cardinal κ,
then F preserves κ-presentable objects.
Moreover, if G : D ⥤ C is fully faithful, then D is locally κ-presentable
(resp κ-accessible) if C is.
In particular, if e : C ≌ D is an equivalence of categories and
C is locally presentable (resp. accessible), then so is D.
theorem CategoryTheory.Adjunction.isCardinalPresentable_leftAdjoint_obj {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : C) [IsCardinalPresentable X κ] [G.IsCardinalAccessible κ] :
IsCardinalPresentable (F.obj X) κ
theorem CategoryTheory.Adjunction.isCardinalFilteredGenerator {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {κ : Cardinal.{w}} [Fact κ.IsRegular] {P : ObjectProperty C} (hP : P.IsCardinalFilteredGenerator κ) [G.IsCardinalAccessible κ] [G.Full] [G.Faithful] :
(P.map F).IsCardinalFilteredGenerator κ
theorem CategoryTheory.Adjunction.hasCardinalFilteredGenerator {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasCardinalFilteredGenerator C κ] [G.IsCardinalAccessible κ] [G.Full] [G.Faithful] :
theorem CategoryTheory.Adjunction.isCardinalLocallyPresentable {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalLocallyPresentable C κ] [G.IsCardinalAccessible κ] [G.Full] [G.Faithful] :
theorem CategoryTheory.Adjunction.isCardinalAccessibleCategory {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] [G.IsCardinalAccessible κ] [G.Full] [G.Faithful] :
theorem CategoryTheory.Equivalence.hasCardinalFilteredGenerator {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (e : C ≌ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasCardinalFilteredGenerator C κ] :
theorem CategoryTheory.Equivalence.isCardinalLocallyPresentable {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (e : C ≌ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalLocallyPresentable C κ] :
theorem CategoryTheory.Equivalence.isCardinalAccessibleCategory {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (e : C ≌ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] :
theorem CategoryTheory.Equivalence.isLocallyPresentable {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (e : C ≌ D) [IsLocallyPresentable.{w, v, u} C] :
theorem CategoryTheory.Equivalence.isAccessibleCategory {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (e : C ≌ D) [IsAccessibleCategory.{w, v, u} C] :