instUniqueHomTopMkId

Mathlib.CategoryTheory.Limits.MorphismProperty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.Over.instUniqueHomTopMkId

Lean4

instance [P.ContainsIdentities] (Y : P.Over ⊤ X) : Unique (Y ⟶ Over.mk ⊤ (𝟙 X) (P.id_mem X))
    where
  default := Over.homMk Y.hom
  uniq
    a := by
    ext
    · simp only [mk_left, homMk_hom, Over.homMk_left]
      rw [← Over.w a]
      simp only [mk_left, Functor.const_obj_obj, mk_hom, Category.comp_id]

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

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

Разделы

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

Аффилиация

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