instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit

English

There is a canonical left Kan extension of F along L given by the pointwise construction, hence HasLeftKanExtension L F.

Русский

Существует каноническое левое кан-расширение F вдоль L, задаваемое покомпонентно, следовательно HasLeftKanExtension L F.

LaTeX

$$$\operatorname{HasLeftKanExtension}(L,F)$$$

Lean4

instance : (pointwiseLeftKanExtension L F).IsLeftKanExtension (pointwiseLeftKanExtensionUnit L F) where
  nonempty_isUniversal := ⟨pointwiseLeftKanExtensionIsUniversal L F⟩

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