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]
: