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)
:
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
Instances For
theorem
CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F : Functor C D}
:
theorem
CategoryTheory.Functor.isFinitelyAccessible_iff_preservesFilteredColimits
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{F : Functor C D}
:
@[reducible, inline]
An object X
is finitely presentable if Hom(X, -)
preserves all filtered colimits.
Equations
Instances For
theorem
CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimits
{C : Type u}
[Category.{v, u} C]
{X : C}
: