isIso_of_isLeftKanExtension

Mathlib.CategoryTheory.Limits.Presheaf

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

English

If a left Kan extension exists, the canonical morphism is an isomorphism.

Русский

Если существует левое Kan-расширение, канонический морфизм является изоморфизмом.

LaTeX

$$$\text{isIso}\;\alpha$ given $L.IsLeftKanExtension \alpha$$$

Lean4

theorem isIso_of_isLeftKanExtension : IsIso α :=
  (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension _ α).isIso_hom

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

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

Разделы

Аффилиация

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