# The category of quivers #

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

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

Category of quivers.

Equations
Instances For
Equations
Equations
• C.str' = C.str

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

Equations
Instances For

Category structure on Quiv

Equations
@[simp]
theorem CategoryTheory.Quiv.forget_map :
∀ {X Y : CategoryTheory.Cat} (F : X Y), = F.toPrefunctor

The forgetful functor from categories to quivers.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Cat.free_map_obj :
∀ {X Y : CategoryTheory.Quiv} (F : X Y) (X_1 : ((fun (V : CategoryTheory.Quiv) => ) X)), ().obj X_1 = F.obj X_1
@[simp]
theorem CategoryTheory.Cat.free_map_map :
∀ {X Y : CategoryTheory.Quiv} (F : X Y) {X_1 Y_1 : ((fun (V : CategoryTheory.Quiv) => ) X)} (f : X_1 Y_1), ().map f =

The functor sending each quiver to its path category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Quiv.lift_obj {V : Type u} [] {C : Type u_1} [] (F : V ⥤q C) (X : ) :
.obj X = F.obj X
@[simp]
theorem CategoryTheory.Quiv.lift_map {V : Type u} [] {C : Type u_1} [] (F : V ⥤q C) :
∀ {X Y : } (f : X Y), .map f = CategoryTheory.composePath (F.mapPath f)
def CategoryTheory.Quiv.lift {V : Type u} [] {C : Type u_1} [] (F : V ⥤q C) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For