isLeftKanExtension

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension

English

The left Kan extension structure on E provides a canonical left Kan extension of L along F.

Русский

Структура левого Кан-расширения на E задаёт каноново лево-расширение для L по F.

LaTeX

$$$E.\\text{IsPointwiseLeftKanExtension} \\Rightarrow E.\\text{IsLeftKanExtension}$$$

Lean4

theorem isLeftKanExtension : E.right.IsLeftKanExtension E.hom where nonempty_isUniversal := ⟨h.isUniversal⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru