The category of quivers #
The category of (bundled) quivers, and the free/forgetful adjunction between Cat
and Quiv
.
Category of quivers.
Equations
Instances For
Equations
Construct a bundled Quiv
from the underlying type and the typeclass.
Instances For
Equations
The forgetful functor from categories to quivers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
The identity in the category of quivers equals the identity prefunctor.
The functor sending each quiver to its path category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An isomorphism of quivers defines an equivalence on carrier types.
Equations
- CategoryTheory.Quiv.equivOfIso e = { toFun := e.hom.obj, invFun := e.inv.obj, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
theorem
CategoryTheory.Quiv.homEquivOfIso_symm_apply
{V W : Quiv}
(e : V ≅ W)
{X Y : ↑V}
(g : e.hom.obj X ⟶ e.hom.obj Y)
:
def
CategoryTheory.Quiv.lift
{V : Type u}
[Quiver V]
{C : Type u_1}
[Category.{u_2, u_1} C]
(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
@[simp]
theorem
CategoryTheory.Quiv.lift_map
{V : Type u}
[Quiver V]
{C : Type u_1}
[Category.{u_2, u_1} C]
(F : V ⥤q C)
{X✝ Y✝ : Paths V}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Quiv.lift_obj
{V : Type u}
[Quiver V]
{C : Type u_1}
[Category.{u_2, u_1} C]
(F : V ⥤q C)
(X : Paths V)
:
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.