preservesColimitsOfSize_of_isLeftKanExtension

English

Left Kan extensions along Yoneda preserve colimits when the target category has enough colimits.

Русский

Левое расширение Кан вдоль Янеда сохраняет колимиты, когда цель обладает нужными колимитами.

LaTeX

$$$\text{PreservesColimitsOfSize}(\mathrm{uliftYoneda.leftKanExtension}\ A)$$$

Lean4

/-- Any left Kan extension along the Yoneda embedding preserves colimits. -/
theorem preservesColimitsOfSize_of_isLeftKanExtension : PreservesColimitsOfSize.{v₃, u₃} L :=
  (uliftYonedaAdjunction L α).leftAdjoint_preservesColimits

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