category

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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

Lean4

/-- The category of bicones on a given diagram. -/
@[simps]
instance category : Category (Bicone F) where
  Hom A B := BiconeMorphism 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