mathlib documentation

category_theory.category.Quiv

The category of quivers #

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

@[protected, instance]
Equations

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

Equations
@[protected, instance]

Category structure on Quiv

Equations

The forgetful functor from categories to quivers.

Equations

The functor sending each quiver to its path category.

Equations

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

Equations

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

Equations