instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable

English

If X is finitely presentable, then coyoneda(obj(op X)) preserves filtered colimits of size.

Русский

Если X является конечной презентируемостью, то ковьонеда(obj(op X)) сохраняет фильтрованные колимиты указанного размера.

LaTeX

$$$(X) [IsFinitelyPresentable\ X] : PreservesFilteredColimitsOfSize(coyoneda.obj(op\ X))$$$

Lean4

instance (X : C) [IsFinitelyPresentable.{w} X] : PreservesFilteredColimitsOfSize.{w, w} (coyoneda.obj (op X)) :=
  by
  rw [← isFinitelyPresentable_iff_preservesFilteredColimitsOfSize]
  infer_instance

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