instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap

English

There exists a left Kan extension along the opposite of a Yoneda-extended functor.

Русский

Существует левое Kan-расширение вдоль противоположного функторa Янеда.

LaTeX

$$$L IsLeftKanExtension α$ for $L$ defined via opposite category.$$

Lean4

/-- Given `F : C ⥤ D` and `X : C`, `yoneda.obj (F.obj X) : Dᵒᵖ ⥤ Type _` is the
left Kan extension of `yoneda.obj X : Cᵒᵖ ⥤ Type _` along `F.op`. -/
instance (X : C) : (yoneda.obj (F.obj X)).IsLeftKanExtension (yonedaMap F X) :=
  ⟨⟨Limits.IsInitial.ofUnique _⟩⟩

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