toCat

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#MonCat.toCat

← MathLib Explorer

English

The functor from MonCat to Cat is full, i.e., every morphism in MonCat is realized by some functor.

Русский

Функтор из MonCat в Cat полон: каждый морфизм MonCat реализуется как функтор.

LaTeX

$$MonCat.toCat.Full$$

Lean4

/-- The fully faithful functor from `MonCat` to `Cat`. -/
def toCat : MonCat ⥤ Cat where
  obj x := Cat.of (SingleObj x)
  map {x y} f := SingleObj.mapHom x y f.hom

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

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

Разделы

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

Аффилиация

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