Categories of presheaves are locally presentable #
If A is a locally κ-presentable category and C is a small category,
we show that Cᵒᵖ ⥤ A is also locally κ-presentable, under the
additional assumption that A has pullbacks (a condition which should
be automatically satisfied (TODO)).
instance
CategoryTheory.Presheaf.instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasCoproducts A]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
(X : C)
(M : A)
[IsCardinalPresentable M κ]
:
IsCardinalPresentable (freeYoneda X M) κ
theorem
CategoryTheory.Presheaf.isStrongGenerator
{A : Type u'}
[Category.{v', u'} A]
{P : ObjectProperty A}
(hP : P.IsStrongGenerator)
[Limits.HasCoproducts A]
[Limits.HasPullbacks A]
(C : Type w)
[SmallCategory C]
:
(ObjectProperty.ofObj fun (T : C × Subtype P) => freeYoneda T.1 ↑T.2).IsStrongGenerator
instance
CategoryTheory.Presheaf.instIsCardinalLocallyPresentableFunctorOppositeOfHasPullbacks
{A : Type u'}
[Category.{v', u'} A]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalLocallyPresentable A κ]
[Limits.HasPullbacks A]
(C : Type w)
[SmallCategory C]
: