instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension

English

Characterization of left Kan extension via preservation of colimits.

Русский

Характеризация левый Kan-расширения через сохранение колимит.

LaTeX

$$$L.IsLeftKanExtension \alpha \iff (IsIso \alpha \land PreservesColimitsOfSize L)$$$

Lean4

instance (L : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ ℰ) [PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂} L]
    [uliftYoneda.{max w v₂}.HasPointwiseLeftKanExtension (uliftYoneda.{max w v₂} ⋙ L)] :
    L.IsLeftKanExtension (𝟙 _ : uliftYoneda.{max w v₂} ⋙ L ⟶ _) :=
  isLeftKanExtension_of_preservesColimits _ (Iso.refl _)

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