Documentation

Mathlib.CategoryTheory.Category.Quiv

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

Instances For

instance CategoryTheory.Quiv.instCoeSortType :

CoeSort Quiv (Type u)

Equations

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

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

Equations

C.str' = C.str

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

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

Equations

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

Instances For

instance CategoryTheory.Quiv.instInhabited :

Equations

CategoryTheory.Quiv.instInhabited = { default := CategoryTheory.Quiv.of (Quiver.Empty PEmpty.{?u.3 + 2}) }

instance CategoryTheory.Quiv.category :

LargeCategory 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 :

Functor Cat Quiv

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.Quiv.forget_obj (C : Cat) :

forget.obj C = of ↑C

@[simp]

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

forget.map F = F.toPrefunctor

theorem CategoryTheory.Quiv.id_eq_id (X : Quiv) :

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 : Quiv} (F : X ⟶ Y) (G : Y ⟶ Z) :

CategoryStruct.comp F G = F ⋙q G

Composition in the category of quivers equals prefunctor composition.

def CategoryTheory.Cat.free :

Functor Quiv Cat

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.Cat.free_obj (V : Quiv) :

free.obj V = of (Paths ↑V)

@[simp]

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

(free.map F).map f = Prefunctor.mapPath F f

@[simp]

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

(free.map F).obj X = F.obj X

def CategoryTheory.Quiv.equivOfIso {V W : 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 := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Quiv.equivOfIso_symm_apply {V W : Quiv} (e : V ≅ W) (a✝ : ↑W) :

(equivOfIso e).symm a✝ = e.inv.obj a✝

@[simp]

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

(equivOfIso e) a✝ = e.hom.obj a✝

@[simp]

theorem CategoryTheory.Quiv.inv_obj_hom_obj_of_iso {V W : 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 : 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 : 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 : 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 : 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.

Instances For

@[simp]

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

(homEquivOfIso e) f = e.hom.map f

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

(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)) :

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.

Instances For

def CategoryTheory.Quiv.lift {V : Type u} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] (F : V ⥤q C) :

Functor (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.

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✝) :

(lift F).map f = composePath (F.mapPath f)

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

(lift F).obj X = F.obj X

def CategoryTheory.Quiv.adj :

Cat.free ⊣ 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.

Instances For