Finitely Presentable Objects

We define finitely presentable objects as a synonym for ℵ₀-presentable objects, and link this definition with the preservation of filtered colimits.

@[reducible, inline]

abbrev CategoryTheory.Functor.IsFinitelyAccessible {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) : Prop

A functor F : C ⥤ D is finitely accessible if it is ℵ₀-accessible. Equivalently, it preserves all filtered colimits. See CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimits.

theorem CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F : Functor C D} : F.IsFinitelyAccessible ↔ Limits.PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F

theorem CategoryTheory.Functor.isFinitelyAccessible_iff_preservesFilteredColimits {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F : Functor C D} : F.IsFinitelyAccessible ↔ Limits.PreservesFilteredColimits F

@[reducible, inline]

abbrev CategoryTheory.IsFinitelyPresentable {C : Type u} [Category.{v, u} C] (X : C) : Prop

An object X is finitely presentable if Hom(X, -) preserves all filtered colimits.

theorem CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimitsOfSize {C : Type u} [Category.{v, u} C] {X : C} : IsFinitelyPresentable X ↔ Limits.PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (coyoneda.obj (Opposite.op X))

theorem CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimits {C : Type u} [Category.{v, u} C] {X : C} : IsFinitelyPresentable X ↔ Limits.PreservesFilteredColimits (coyoneda.obj (Opposite.op X))

theorem CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize {C : Type u} [Category.{v, u} C] : HasCardinalFilteredColimits C Cardinal.aleph0 ↔ Limits.HasFilteredColimitsOfSize.{w, w, v, u} C

theorem CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimits {C : Type u} [Category.{v, u} C] : HasCardinalFilteredColimits C Cardinal.aleph0 ↔ Limits.HasFilteredColimits C