instHasRightKanExtension

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

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

English

There is a canonical instance providing a right Kan extension structure for L and F.

Русский

Существует каноническая структура правого кан-расширения для L и F.

LaTeX

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

Lean4

instance : HasRightKanExtension L F :=
  HasRightKanExtension.mk _ (pointwiseRightKanExtensionCounit L F)

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

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

Разделы

Аффилиация

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