isColimitChangeEmptyCocone

Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.isColimitChangeEmptyCocone

Lean4

/-- Being initial is independent of the empty diagram, its universe, and the cocone over it,
    as long as the cocone points are isomorphic. -/
def isColimitChangeEmptyCocone {c₁ : Cocone F₁} (hl : IsColimit c₁) (c₂ : Cocone F₂) (hi : c₁.pt ≅ c₂.pt) : IsColimit c₂
    where
  desc c := hi.inv ≫ hl.desc ⟨c.pt, by cat_disch, by simp⟩
  uniq c f
    _ := by
    dsimp
    rw [← hl.uniq _ (hi.hom ≫ f) _]
    · simp only [Iso.inv_hom_id_assoc]
    · simp

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

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

Разделы

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

Аффилиация

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