categoryStruct

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SingleObj.categoryStruct

Lean4

/-- One and `flip (*)` become `id` and `comp` for morphisms of the single object category. -/
instance categoryStruct [One M] [Mul M] : CategoryStruct (SingleObj M)
    where
  Hom _ _ := M
  comp x y := y * x
  id _ := 1

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

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

Разделы

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

Аффилиация

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