free

Mathlib.CategoryTheory.Category.Quiv

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cat.free

Lean4

/-- The functor sending each quiver to its path category. -/
@[simps]
def free : Quiv.{v, u} ⥤ Cat.{max u v, u} where
  obj V := Cat.of (Paths V)
  map F := Functor.toCatHom (freeMap (Prefunctor.ofQuivHom F))
  map_id _ := freeMap_id _
  map_comp _ _ := freeMap_comp _ _

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

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

Разделы

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

Аффилиация

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