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

• CategoryTheory.Quiv = CategoryTheory.Bundled Quiver

instance CategoryTheory.Quiv.instCoeSortType : CoeSort CategoryTheory.Quiv (Type u)

Equations

• CategoryTheory.Quiv.instCoeSortType = { coe := CategoryTheory.Bundled.α }

instance CategoryTheory.Quiv.str' (C : CategoryTheory.Quiv) : Quiver ↑C

Equations

• C.str' = C.str

def CategoryTheory.Quiv.of (C : Type u) [Quiver C] : CategoryTheory.Quiv

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

Equations

• CategoryTheory.Quiv.of C = CategoryTheory.Bundled.of C

instance CategoryTheory.Quiv.instInhabited : Inhabited CategoryTheory.Quiv

Equations

• CategoryTheory.Quiv.instInhabited = { default := CategoryTheory.Quiv.of (Quiver.Empty PEmpty.{u_1 + 2} ) }

instance CategoryTheory.Quiv.category : CategoryTheory.LargeCategory CategoryTheory.Quiv

Category structure on Quiv

Equations

• CategoryTheory.Quiv.category = CategoryTheory.Category.mk @CategoryTheory.Quiv.category.proof_1 @CategoryTheory.Quiv.category.proof_1 @CategoryTheory.Quiv.category.proof_2

@[simp]

theorem CategoryTheory.Quiv.forget_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y), CategoryTheory.Quiv.forget.map F = F.toPrefunctor

@[simp]

theorem CategoryTheory.Quiv.forget_obj (C : CategoryTheory.Cat) : CategoryTheory.Quiv.forget.obj C = CategoryTheory.Quiv.of ↑C

def CategoryTheory.Quiv.forget : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Quiv

The forgetful functor from categories to quivers.

Equations

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

@[simp]

theorem CategoryTheory.Cat.free_obj (V : CategoryTheory.Quiv) : CategoryTheory.Cat.free.obj V = CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)

@[simp]

theorem CategoryTheory.Cat.free_map_obj : ∀ {X Y : CategoryTheory.Quiv} (F : X ⟶ Y) (X_1 : ↑((fun (V : CategoryTheory.Quiv) => CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)) X)), (CategoryTheory.Cat.free.map F).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) => CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)) X)} (f : X_1 ⟶ Y_1), (CategoryTheory.Cat.free.map F).map f = Prefunctor.mapPath F f

def CategoryTheory.Cat.free : CategoryTheory.Functor CategoryTheory.Quiv CategoryTheory.Cat

The functor sending each quiver to its path category.

Equations

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

@[simp]

theorem CategoryTheory.Quiv.lift_obj {V : Type u} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : V ⥤q C) (X : CategoryTheory.Paths V) : (CategoryTheory.Quiv.lift F).obj X = F.obj X

@[simp]

theorem CategoryTheory.Quiv.lift_map {V : Type u} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : V ⥤q C) : ∀ {X Y : CategoryTheory.Paths V} (f : X ⟶ Y), (CategoryTheory.Quiv.lift F).map f = CategoryTheory.composePath (F.mapPath f)

def CategoryTheory.Quiv.lift {V : Type u} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : V ⥤q C) : CategoryTheory.Functor (CategoryTheory.Paths V) 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.

def CategoryTheory.Quiv.adj : CategoryTheory.Cat.free ⊣ CategoryTheory.Quiv.forget

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.