isIso_π_initial

Mathlib.CategoryTheory.Limits.Shapes.Terminal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.isIso_π_initial

English

For a category with an initial J, the map π_F (⊥ J) is an isomorphism.

Русский

Для категории с начальным объектом J отображение π_F(⊥ J) является изоморфизмом.

LaTeX

$$$$\\mathrm{IsIso}(\\mathrm{limit}.\\pi F (\\perp_J)).$$$$

Lean4

instance isIso_π_initial [HasInitial J] (F : J ⥤ C) : IsIso (limit.π F (⊥_ J)) :=
  isIso_π_of_isInitial initialIsInitial F

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

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

Разделы

Аффилиация

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