freeMap

Mathlib.CategoryTheory.Category.Quiv

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

Lean4

/-- A prefunctor `V ⥤q W` induces a functor between the path categories defined by `F.mapPath`. -/
@[simps]
def freeMap {V W : Type*} [Quiver V] [Quiver W] (F : V ⥤q W) : Paths V ⥤ Paths W
    where
  obj := F.obj
  map := F.mapPath
  map_comp f g := F.mapPath_comp f g

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

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

Разделы

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

Аффилиация

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