category

Mathlib.CategoryTheory.Limits.Cones

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

Lean4

/-- The category of cones on a given diagram. -/
@[simps]
instance category : Category (Cone F) where
  Hom A B := ConeMorphism A B
  comp f g := { hom := f.hom ≫ g.hom }
  id
    B :=
    { hom := 𝟙 B.pt }
      /- We do not want `simps` automatically generate the lemma for simplifying the
      hom field of a category. So we need to write the `ext` lemma in terms of the
      categorical morphism, rather than the underlying structure. -/

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

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

Разделы

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

Аффилиация

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