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.

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

@[implicit_reducible]

instance CategoryTheory.Quiv.instInhabited : Inhabited Quiv

@[implicit_reducible]

instance CategoryTheory.Quiv.category : LargeCategory Quiv

Category structure on Quiv

def CategoryTheory.Quiv.forget : Functor Cat Quiv

The forgetful functor from categories to quivers.

@[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.toFunctor.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.Prefunctor.toQuivHom {C D : Type u} [Quiver C] [Quiver D] (F : C ⥤q D) : Quiv.of C ⟶ Quiv.of D

Prefunctors between quivers define arrows in Quiv.

def CategoryTheory.Prefunctor.ofQuivHom {C D : Quiv} (F : C ⟶ D) : ↑C ⥤q ↑D

Arrows in Quiv define prefunctors.

@[simp]

theorem CategoryTheory.Prefunctor.to_ofQuivHom {C D : Quiv} (F : C ⟶ D) : toQuivHom (ofQuivHom F) = F

@[simp]

theorem CategoryTheory.Prefunctor.of_toQuivHom {C D : Type} [Quiver C] [Quiver D] (F : C ⥤q D) : ofQuivHom (toQuivHom F) = F

def CategoryTheory.Cat.freeMap {V : Type u_1} {W : Type u_2} [Quiver V] [Quiver W] (F : V ⥤q W) : Functor (Paths V) (Paths W)

A prefunctor V ⥤q W induces a functor between the path categories defined by F.mapPath.

@[simp]

theorem CategoryTheory.Cat.freeMap_obj {V : Type u_1} {W : Type u_2} [Quiver V] [Quiver W] (F : V ⥤q W) (a✝ : V) : (freeMap F).obj a✝ = F.obj a✝

@[simp]

theorem CategoryTheory.Cat.freeMap_map {V : Type u_1} {W : Type u_2} [Quiver V] [Quiver W] (F : V ⥤q W) {X✝ Y✝ : Paths V} (a✝ : Quiver.Path X✝ Y✝) : (freeMap F).map a✝ = F.mapPath a✝

def CategoryTheory.Cat.freeMapIdIso (V : Type u_1) [Quiver V] : freeMap (𝟭q V) ≅ Functor.id (Paths V)

The functor free : Quiv ⥤ Cat preserves identities up to natural isomorphism and in fact up to equality.

@[simp]

theorem CategoryTheory.Cat.freeMapIdIso_inv_app (V : Type u_1) [Quiver V] (X : Paths V) : (freeMapIdIso V).inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Cat.freeMapIdIso_hom_app (V : Type u_1) [Quiver V] (X : Paths V) : (freeMapIdIso V).hom.app X = CategoryStruct.id X

theorem CategoryTheory.Cat.freeMap_id (V : Type u_1) [Quiver V] : freeMap (𝟭q V) = Functor.id (Paths V)

def CategoryTheory.Cat.freeMapCompIso {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [Quiver V₁] [Quiver V₂] [Quiver V₃] (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) : freeMap (F ⋙q G) ≅ (freeMap F).comp (freeMap G)

The functor free : Quiv ⥤ Cat preserves composition up to natural isomorphism and in fact up to equality.

@[simp]

theorem CategoryTheory.Cat.freeMapCompIso_hom_app {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [Quiver V₁] [Quiver V₂] [Quiver V₃] (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) (X : Paths V₁) : (freeMapCompIso F G).hom.app X = CategoryStruct.id (G.obj (F.obj X))

@[simp]

theorem CategoryTheory.Cat.freeMapCompIso_inv_app {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [Quiver V₁] [Quiver V₂] [Quiver V₃] (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) (X : Paths V₁) : (freeMapCompIso F G).inv.app X = CategoryStruct.id (G.obj (F.obj X))

theorem CategoryTheory.Cat.freeMap_comp {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [Quiver V₁] [Quiver V₂] [Quiver V₃] (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) : freeMap (F ⋙q G) = (freeMap F).comp (freeMap G)

def CategoryTheory.Cat.free : Functor Quiv Cat

The functor sending each quiver to its path category.

@[simp]

theorem CategoryTheory.Cat.free_map {X✝ Y✝ : Quiv} (F : X✝ ⟶ Y✝) : free.map F = (freeMap (Prefunctor.ofQuivHom F)).toCatHom

@[simp]

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

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

An isomorphism of quivers defines an equivalence on carrier types.

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

@[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)) : of V ≅ of W

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

def CategoryTheory.Quiv.lift {V : Type u} [Quiver V] {C : Type u₁} [Category.{v₁, u₁} C] (F : V ⥤q C) : Functor (Paths V) C

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

@[simp]

theorem CategoryTheory.Quiv.lift_map {V : Type u} [Quiver V] {C : Type u₁} [Category.{v₁, u₁} 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₁} [Category.{v₁, u₁} C] (F : V ⥤q C) (X : Paths V) : (lift F).obj X = F.obj X

def CategoryTheory.Quiv.pathCompositionNaturality {C : Type u} {D : Type u₁} [Category.{v, u} C] [Category.{v₁, u₁} D] (F : Functor C D) : (Cat.freeMap F.toPrefunctor).comp (pathComposition D) ≅ (pathComposition C).comp F

Naturality of pathComposition.

theorem CategoryTheory.Quiv.pathComposition_naturality {C : Type u} {D : Type u₁} [Category.{v, u} C] [Category.{v₁, u₁} D] (F : Functor C D) : (Cat.freeMap F.toPrefunctor).comp (pathComposition D) = (pathComposition C).comp F

Naturality of pathComposition, which defines a natural transformation Quiv.forget ⋙ Cat.free ⟶ 𝟭 _.

theorem CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor {V : Type u} {W : Type u₁} [Quiver V] [Quiver W] (F : V ⥤q W) : Paths.of V ⋙q (Cat.freeMap F).toPrefunctor = F ⋙q Paths.of W

Naturality of Paths.of, which defines a natural transformation 𝟭 _⟶ Cat.free ⋙ Quiv.forget.

def CategoryTheory.Quiv.freeMapPathsOfCompPathCompositionIso (V : Type u) [Quiver V] : (Cat.freeMap (Paths.of V)).comp (pathComposition (Paths V)) ≅ Functor.id (Paths V)

The left triangle identity of Cat.free ⊣ Quiv.forget as a natural isomorphism

theorem CategoryTheory.Quiv.freeMap_pathsOf_pathComposition (V : Type u) [Quiver V] : (Cat.freeMap (Paths.of V)).comp (pathComposition (Paths V)) = Functor.id (Paths V)

theorem CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor (C : Type u) [Category.{v, u} C] : Paths.of C ⋙q (pathComposition C).toPrefunctor = 𝟭q C

An unbundled version of the right triangle equality.

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

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

def CategoryTheory.Quiv.pathsEquiv {V : Type u} {C : Type u₁} [Quiver V] [Category.{v₁, u₁} C] : Functor (Paths V) C ≃ V ⥤q C

The universal property of the path category of a quiver.

@[simp]

theorem CategoryTheory.Quiv.adj_homEquiv {V C : Type u} [Quiver V] [Category.{max u v, u} C] : adj.homEquiv (of V) (Cat.of C) = (Cat.Hom.equivFunctor (Cat.of (Paths V)) (Cat.of C)).trans pathsEquiv