# mathlib3documentation

category_theory.category.Quiv

# The category of quivers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[nolint]
def category_theory.Quiv  :
Type (max (u+1) u (v+1))

Category of quivers.

Equations
Instances for category_theory.Quiv
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations
@[protected, instance]
Equations
@[protected, instance]

Category structure on Quiv

Equations
@[simp]
@[simp]

The forgetful functor from categories to quivers.

Equations
@[simp]
theorem category_theory.Cat.free_map_map (V W : category_theory.Quiv) (F : V W) (X Y : ) (f : X Y) :
@[simp]
@[simp]
theorem category_theory.Cat.free_map_obj (V W : category_theory.Quiv) (F : V W) (X : ) :
= F.obj X

The functor sending each quiver to its path category.

Equations
def category_theory.Quiv.lift {V : Type u} [quiver V] {C : Type u_1} (F : V ⥤q C) :

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

Equations
@[simp]
theorem category_theory.Quiv.lift_map {V : Type u} [quiver V] {C : Type u_1} (F : V ⥤q C) (X Y : category_theory.paths V) (f : X Y) :
@[simp]
theorem category_theory.Quiv.lift_obj {V : Type u} [quiver V] {C : Type u_1} (F : V ⥤q C) (X : category_theory.paths V) :
= F.obj X

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

Equations