isFinitelyPresentable_iff_preservesFilteredColimits

English

For any object X, IsFinitelyPresentable X is equivalent to preserving filtered colimits of the coyoneda functor at X.

Русский

Для любого объекта X, IsFinitelyPresentable X эквивалентно сохранению фильтрованных колимитов ковьонеды в X.

LaTeX

$$$IsFinitelyPresentable X \iff PreservesFilteredColimits(\mathrm{coyoneda.obj}(\mathrm{op} X))$$$

Lean4

theorem isFinitelyPresentable_iff_preservesFilteredColimits {X : C} :
    IsFinitelyPresentable.{v} X ↔ PreservesFilteredColimits (coyoneda.obj (op X)) :=
  Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

Похожие утверждения