instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda

Mathlib.CategoryTheory.Limits.Presheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presheaf.instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda

English

If L preserves colimits, then it is a left Kan extension along an iso.

Русский

Если L сохраняет колимиты, то он левое Kan-расширение вдоль изоморфизма.

LaTeX

$$$L.IsLeftKanExtension(\alpha)$ iff $\text{IsIso}(\alpha) \land \text{PreservesColimitsOfSize}(L)$$$

Lean4

instance : IsIso (uliftYoneda.{max w v₂}.leftKanExtensionUnit A) :=
  isIso_of_isLeftKanExtension _ (uliftYoneda.leftKanExtensionUnit A)

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

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

Разделы

Аффилиация

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