instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit

Mathlib.CategoryTheory.Functor.KanExtension.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit

English

The unit of the left Kan extension along L is an equivalence when evaluated at F.

Русский

Единица левго Кан-расширения вдоль L является эквивалентностью при применении к F.

LaTeX

$$$(L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)$$$

Lean4

instance : (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F) where
  nonempty_isUniversal := ⟨initialIsInitial⟩

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

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

Разделы

Аффилиация

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