preservesColimitsOfSize_leftKanExtension

English

If L is a left Kan extension data, then it preserves colimits.

Русский

Если L задан как левое Kan-расширение, он сохраняет колимиты.

LaTeX

$$$\text{preservesColimitsOfSize } L$$$

Lean4

/-- See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties. -/
instance preservesColimitsOfSize_leftKanExtension :
    PreservesColimitsOfSize.{v₃, u₃} (uliftYoneda.{max w v₂}.leftKanExtension A) :=
  (uliftYonedaAdjunction _ (uliftYoneda.leftKanExtensionUnit A)).leftAdjoint_preservesColimits

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