isLimitChangeEmptyCone

Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

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

Lean4

/-- Being terminal is independent of the empty diagram, its universe, and the cone over it,
    as long as the cone points are isomorphic. -/
def isLimitChangeEmptyCone {c₁ : Cone F₁} (hl : IsLimit c₁) (c₂ : Cone F₂) (hi : c₁.pt ≅ c₂.pt) : IsLimit c₂
    where
  lift c := hl.lift ⟨c.pt, by cat_disch, by simp⟩ ≫ hi.hom
  uniq c f
    _ := by
    dsimp
    rw [← hl.uniq _ (f ≫ hi.inv) _]
    · simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]
    · simp

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

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

Разделы

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

Аффилиация

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