isIso_ι_of_isColimit

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit

← MathLib Explorer

English

If c is a colimit cocone for F, then c.ι.app i0 is an isomorphism.

Русский

Если c — колимитный конус для F, то c.ι.app i0 — изоморфизм.

LaTeX

$$IsIso(c.ι.app i_0)$$

Lean4

theorem isIso_ι_of_isColimit {c : Cocone F} (hc : IsColimit c) : IsIso (c.ι.app i₀) :=
  by
  simp only [← IsColimit.comp_coconePointUniqueUpToIso_inv hc h.isColimitCocone i₀, cocone_ι_app, coconeιApp_eq_id,
    id_comp]
  infer_instance

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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