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.

Equations

• F.IsFinitelyAccessible = F.IsCardinalAccessible Cardinal.aleph0

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.

Equations

• CategoryTheory.IsFinitelyPresentable X = CategoryTheory.IsCardinalPresentable X Cardinal.aleph0

def CategoryTheory.ObjectProperty.isFinitelyPresentable (C : Type u) [Category.{v, u} C] : ObjectProperty C

IsFinitelyPresentable as an ObjectProperty on C. This is sometimes called "compact".

Equations

• CategoryTheory.ObjectProperty.isFinitelyPresentable C X = CategoryTheory.IsFinitelyPresentable X

theorem CategoryTheory.ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable {C : Type u} [Category.{v, u} C] : isFinitelyPresentable C = isCardinalPresentable C Cardinal.aleph0

def CategoryTheory.MorphismProperty.isFinitelyPresentable (C : Type u) [Category.{v, u} C] : MorphismProperty C

A morphism f : X ⟶ Y is finitely presentable if it is so as an object of Under X.

Equations

• CategoryTheory.MorphismProperty.isFinitelyPresentable C f = CategoryTheory.ObjectProperty.isFinitelyPresentable (CategoryTheory.Under x✝¹) (CategoryTheory.Under.mk f)

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))

instance CategoryTheory.instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable {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))

instance CategoryTheory.instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι {C : Type u} [Category.{v, u} C] (X : (ObjectProperty.isFinitelyPresentable C).FullSubcategory) : IsFinitelyPresentable ((ObjectProperty.isFinitelyPresentable C).ι.obj X)

theorem CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] [IsFiltered J] {D : Functor J C} {c : Limits.Cocone D} (hc : Limits.IsColimit c) {X : C} [IsFinitelyPresentable X] (f : X ⟶ c.pt) : ∃ (j : J) (p : X ⟶ D.obj j), CategoryStruct.comp p (c.ι.app j) = f

theorem CategoryTheory.IsFinitelyPresentable.exists_eq_of_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] [IsFiltered J] {D : Functor J C} {c : Limits.Cocone D} (hc : Limits.IsColimit c) {X : C} [IsFinitelyPresentable X] {i j : J} (f : X ⟶ D.obj i) (g : X ⟶ D.obj j) (h : CategoryStruct.comp f (c.ι.app i) = CategoryStruct.comp g (c.ι.app j)) : ∃ (k : J) (u : i ⟶ k) (v : j ⟶ k), CategoryStruct.comp f (D.map u) = CategoryStruct.comp g (D.map v)

theorem CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] [IsFiltered J] {D : Functor J C} {c : Limits.Cocone D} (hc : Limits.IsColimit c) {X A : C} (p : X ⟶ A) (s : (Functor.const J).obj X ⟶ D) [IsFinitelyPresentable (Under.mk p)] (f : A ⟶ c.pt) (h : ∀ (j : J), CategoryStruct.comp (s.app j) (c.ι.app j) = CategoryStruct.comp p f) : ∃ (j : J) (q : A ⟶ D.obj j), CategoryStruct.comp p q = s.app j ∧ CategoryStruct.comp q (c.ι.app j) = f

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