isFinitelyPresentable_iff_preservesFilteredColimitsOfSize

English

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

Русский

Для произвольного объекта X условие IsFinitelyPresentable X эквивалентно сохранению фильтрованных колимитов для ковёнойды-функторов в X.

LaTeX

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

Lean4

theorem isFinitelyPresentable_iff_preservesFilteredColimitsOfSize {X : C} :
    IsFinitelyPresentable.{w} X ↔ PreservesFilteredColimitsOfSize.{w, w} (coyoneda.obj (op X)) :=
  Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

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