mathlib3 documentation

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.

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

Category of quivers.

Equations
Instances for category_theory.Quiv
source
@[protected, instance]
def category_theory.Quiv.has_coe_to_sort  :
has_coe_to_sort category_theory.Quiv (Type u)
Equations
source
@[protected, instance]
def category_theory.Quiv.str (C : category_theory.Quiv) :
quiver ↥C
Equations
source
def category_theory.Quiv.of (C : Type u) [quiver C] :
category_theory.Quiv

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

Equations
source
@[protected, instance]
def category_theory.Quiv.inhabited  :
inhabited category_theory.Quiv
Equations
source
@[protected, instance]
def category_theory.Quiv.category  :
category_theory.large_category category_theory.Quiv

Category structure on Quiv

Equations
source
@[simp]
theorem category_theory.Quiv.forget_map (C D : category_theory.Cat) (F : C ⟶ D) :
category_theory.Quiv.forget.map F = category_theory.functor.to_prefunctor F
source
@[simp]
theorem category_theory.Quiv.forget_obj (C : category_theory.Cat) :
category_theory.Quiv.forget.obj C = category_theory.Quiv.of ↥C
source
def category_theory.Quiv.forget  :
category_theory.Cat ⥤ category_theory.Quiv

The forgetful functor from categories to quivers.

Equations
source
@[simp]
theorem category_theory.Cat.free_map_map (V W : category_theory.Quiv) (F : V ⟶ W) (X Y : ↥(category_theory.Cat.of (category_theory.paths ↥V))) (f : X ⟶ Y) :
(category_theory.Cat.free.map F).map f = prefunctor.map_path F f
source
@[simp]
theorem category_theory.Cat.free_obj (V : category_theory.Quiv) :
category_theory.Cat.free.obj V = category_theory.Cat.of (category_theory.paths ↥V)
source
@[simp]
theorem category_theory.Cat.free_map_obj (V W : category_theory.Quiv) (F : V ⟶ W) (X : ↥(category_theory.Cat.of (category_theory.paths ↥V))) :
(category_theory.Cat.free.map F).obj X = F.obj X
source
def category_theory.Cat.free  :
category_theory.Quiv ⥤ category_theory.Cat

The functor sending each quiver to its path category.

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

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

Equations
source
@[simp]
theorem category_theory.Quiv.lift_map {V : Type u} [quiver V] {C : Type u_1} [category_theory.category C] (F : V ⥤q C) (X Y : category_theory.paths V) (f : X ⟶ Y) :
(category_theory.Quiv.lift F).map f = category_theory.compose_path (F.map_path f)
source
@[simp]
theorem category_theory.Quiv.lift_obj {V : Type u} [quiver V] {C : Type u_1} [category_theory.category C] (F : V ⥤q C) (X : category_theory.paths V) :
(category_theory.Quiv.lift F).obj X = F.obj X
source
def category_theory.Quiv.adj  :
category_theory.Cat.free ⊣ category_theory.Quiv.forget

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

Equations