mathlib documentation

category_theory.category.Quiv

The category of quivers #

The category of (bundled) quivers, and the free/forgetful adjunction between Cat and Quiv.

def category_theory.Quiv  :
Type (max (u+1) u (v+1))

Category of quivers.

Equations
@[instance]
Equations

Construct a bundled Quiv from the underlying type and the typeclass.

Equations
@[instance]

Category structure on Quiv

Equations

The forgetful functor from categories to quivers.

Equations

The functor sending each quiver to its path category.

Equations
def category_theory.Quiv.lift {V : Type u} [quiver V] {C : Type u} [category_theory.category C] (F : prefunctor V C) :

Any prefunctor into a category lifts to a functor from the path category.

Equations
@[simp]
theorem category_theory.Quiv.lift_obj {V : Type u} [quiver V] {C : Type u} [category_theory.category C] (F : prefunctor V C) (X : category_theory.paths V) :

The adjunction between forming the free category on a quiver, and forgetting a category to a quiver.

Equations