biconeCategoryStruct

Mathlib.CategoryTheory.Limits.Bicones

URI: https://scilib.ai/kg/mathlib#CategoryTheory.biconeCategoryStruct

Lean4

@[simps]
instance biconeCategoryStruct : CategoryStruct (Bicone J)
    where
  Hom := BiconeHom J
  id j := Bicone.casesOn j BiconeHom.left_id BiconeHom.right_id fun k => BiconeHom.diagram (𝟙 k)
  comp f
    g := by
    rcases f with (_ | _ | _ | _ | f)
    · exact g
    · exact g
    · cases g
      apply BiconeHom.left
    · cases g
      apply BiconeHom.right
    · rcases g with (_ | _ | _ | _ | g)
      exact BiconeHom.diagram (f ≫ g)

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

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

Разделы

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

Аффилиация

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