instSmallCategoryElemObj

Mathlib.CategoryTheory.SmallRepresentatives

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj

English

There is a canonical SmallCategory structure on the elements of a SmallCategoryOfSet Ω.

Русский

Существует каноническая структура SmallCategory на элементах SmallCategoryOfSet Ω.

LaTeX

$$$\\text{SmallCategory}(S.\\mathrm{Elem})$$$

Lean4

@[simps]
instance (S : SmallCategoryOfSet Ω) : SmallCategory S.obj
    where
  Hom X Y := S.hom X Y
  id := S.id
  comp := S.comp

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

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

Разделы

Аффилиация

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