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.3 + 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

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.Quiv.forget_obj (C : CategoryTheory.Cat) : CategoryTheory.Quiv.forget.obj C = CategoryTheory.Quiv.of ↑C

@[simp]

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

theorem CategoryTheory.Quiv.id_eq_id (X : CategoryTheory.Quiv) : CategoryTheory.CategoryStruct.id X = 𝟭q ↑X

The identity in the category of quivers equals the identity prefunctor.

theorem CategoryTheory.Quiv.comp_eq_comp {X Y Z : CategoryTheory.Quiv} (F : X ⟶ Y) (G : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp F G = F ⋙q G

Composition in the category of quivers equals prefunctor composition.

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.Cat.free_obj (V : CategoryTheory.Quiv) : CategoryTheory.Cat.free.obj V = CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)

@[simp]

theorem CategoryTheory.Cat.free_map_map {X✝ Y✝ : CategoryTheory.Quiv} (F : X✝ ⟶ Y✝) {X✝¹ Y✝¹ : ↑((fun (V : CategoryTheory.Quiv) => CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)) X✝)} (f : X✝¹ ⟶ Y✝¹) : (CategoryTheory.Cat.free.map F).map f = Prefunctor.mapPath F f

@[simp]

theorem CategoryTheory.Cat.free_map_obj {X✝ Y✝ : CategoryTheory.Quiv} (F : X✝ ⟶ Y✝) (X : ↑((fun (V : CategoryTheory.Quiv) => CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)) X✝)) : (CategoryTheory.Cat.free.map F).obj X = F.obj X

def CategoryTheory.Quiv.equivOfIso {V W : CategoryTheory.Quiv} (e : V ≅ W) : ↑V ≃ ↑W

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 := ⋯ }

@[simp]

theorem CategoryTheory.Quiv.equivOfIso_symm_apply {V W : CategoryTheory.Quiv} (e : V ≅ W) (a✝ : ↑W) : (CategoryTheory.Quiv.equivOfIso e).symm a✝ = e.inv.obj a✝

@[simp]

theorem CategoryTheory.Quiv.equivOfIso_apply {V W : CategoryTheory.Quiv} (e : V ≅ W) (a✝ : ↑V) : (CategoryTheory.Quiv.equivOfIso e) a✝ = e.hom.obj a✝

@[simp]

theorem CategoryTheory.Quiv.inv_obj_hom_obj_of_iso {V W : CategoryTheory.Quiv} (e : V ≅ W) (X : ↑V) : e.inv.obj (e.hom.obj X) = X

@[simp]

theorem CategoryTheory.Quiv.hom_obj_inv_obj_of_iso {V W : CategoryTheory.Quiv} (e : V ≅ W) (Y : ↑W) : e.hom.obj (e.inv.obj Y) = Y

theorem CategoryTheory.Quiv.hom_map_inv_map_of_iso {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑W} (f : X ⟶ Y) : e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

theorem CategoryTheory.Quiv.inv_map_hom_map_of_iso {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} (f : X ⟶ Y) : e.inv.map (e.hom.map f) = Quiver.homOfEq f ⋯ ⋯

def CategoryTheory.Quiv.homEquivOfIso {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} : (X ⟶ Y) ≃ (e.hom.obj X ⟶ e.hom.obj Y)

An isomorphism of quivers defines an equivalence on hom types.

Equations

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

@[simp]

theorem CategoryTheory.Quiv.homEquivOfIso_apply {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} (f : X ⟶ Y) : (CategoryTheory.Quiv.homEquivOfIso e) f = e.hom.map f

@[simp]

theorem CategoryTheory.Quiv.homEquivOfIso_symm_apply {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} (g : e.hom.obj X ⟶ e.hom.obj Y) : (CategoryTheory.Quiv.homEquivOfIso e).symm g = Quiver.homOfEq (e.inv.map g) ⋯ ⋯

@[simp]

theorem CategoryTheory.Quiv.homOfEq_map_homOfEq {V W : Type u} [Quiver V] [Quiver W] (e : V ≃ W) (he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') {X'' Y'' : W} (hX' : e X' = X'') (hY' : e Y' = Y'') : Quiver.homOfEq ((he X' Y') (Quiver.homOfEq f hX hY)) hX' hY' = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

def CategoryTheory.Quiv.isoOfEquiv {V W : Type u} [Quiver V] [Quiver W] (e : V ≃ W) (he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) : CategoryTheory.Quiv.of V ≅ CategoryTheory.Quiv.of W

Compatible equivalences of types and hom-types induce an isomorphism of quivers.

Equations

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

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.

@[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)

@[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

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.