commaCategory

Mathlib.CategoryTheory.Comma.Basic

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

Lean4

instance commaCategory : Category (Comma L R)
    where
  Hom X Y := CommaMorphism X Y
  id
    X :=
    { left := 𝟙 X.left
      right := 𝟙 X.right }
  comp f
    g :=
    { left := f.left ≫ g.left
      right := f.right ≫ g.right }

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

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

Разделы

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

Аффилиация

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