# The category paths on a quiver. #

When C is a quiver, paths C is the category of paths.

## When the quiver is itself a category #

We provide path_composition : paths C ⥤ C.

We check that the quotient of the path category of a category by the canonical relation (paths are related if they compose to the same path) is equivalent to the original category.

def CategoryTheory.Paths (V : Type u₁) :
Type u₁

A type synonym for the category of paths in a quiver.

Equations
Instances For
instance CategoryTheory.instInhabitedPaths (V : Type u₁) [] :
Equations
• = { default := default }
instance CategoryTheory.Paths.categoryPaths (V : Type u₁) [] :
Equations
@[simp]
theorem CategoryTheory.Paths.of_map {V : Type u₁} [] :
∀ {X Y : V} (f : X Y), CategoryTheory.Paths.of.map f = f.toPath
@[simp]
theorem CategoryTheory.Paths.of_obj {V : Type u₁} [] (X : V) :
CategoryTheory.Paths.of.obj X = X
def CategoryTheory.Paths.of {V : Type u₁} [] :

The inclusion of a quiver V into its path category, as a prefunctor.

Equations
• CategoryTheory.Paths.of = { obj := fun (X : V) => X, map := fun {X Y : V} (f : X Y) => f.toPath }
Instances For
def CategoryTheory.Paths.lift {V : Type u₁} [] {C : Type u_1} [] (φ : V ⥤q C) :

Any prefunctor from V lifts to a functor from paths V

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Paths.lift_nil {V : Type u₁} [] {C : Type u_1} [] (φ : V ⥤q C) (X : V) :
.map Quiver.Path.nil = CategoryTheory.CategoryStruct.id (φ.obj X)
@[simp]
theorem CategoryTheory.Paths.lift_cons {V : Type u₁} [] {C : Type u_1} [] (φ : V ⥤q C) {X : V} {Y : V} {Z : V} (p : ) (f : Y Z) :
.map (p.cons f) = CategoryTheory.CategoryStruct.comp (.map p) (φ.map f)
@[simp]
theorem CategoryTheory.Paths.lift_toPath {V : Type u₁} [] {C : Type u_1} [] (φ : V ⥤q C) {X : V} {Y : V} (f : X Y) :
.map f.toPath = φ.map f
theorem CategoryTheory.Paths.lift_spec {V : Type u₁} [] {C : Type u_1} [] (φ : V ⥤q C) :
CategoryTheory.Paths.of ⋙q .toPrefunctor = φ
theorem CategoryTheory.Paths.lift_unique {V : Type u₁} [] {C : Type u_1} [] (φ : V ⥤q C) (Φ : ) (hΦ : CategoryTheory.Paths.of ⋙q Φ.toPrefunctor = φ) :
theorem CategoryTheory.Paths.ext_functor {V : Type u₁} [] {C : Type u_1} [] {F : } {G : } (h_obj : F.obj = G.obj) (h : ∀ (a b : V) (e : a b), F.map e.toPath = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.map e.toPath) )) :
F = G

Two functors out of a path category are equal when they agree on singleton paths.

@[simp]
theorem CategoryTheory.Prefunctor.mapPath_comp' (V : Type u₁) [] (W : Type u₂) [] (F : V ⥤q W) {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
F.mapPath = (F.mapPath f).comp (F.mapPath g)
def CategoryTheory.composePath {C : Type u₁} [] {X : C} {Y : C} :
(X Y)

A path in a category can be composed to a single morphism.

Equations
Instances For
@[simp]
theorem CategoryTheory.composePath_nil {C : Type u₁} [] {X : C} :
CategoryTheory.composePath Quiver.Path.nil =
@[simp]
theorem CategoryTheory.composePath_cons {C : Type u₁} [] {X : C} {Y : C} {Z : C} (p : ) (e : Y Z) :
@[simp]
theorem CategoryTheory.composePath_toPath {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.composePath_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : ) (g : ) :
@[simp]
theorem CategoryTheory.composePath_id {C : Type u₁} [] {X : } :
@[simp]
theorem CategoryTheory.composePath_comp' {C : Type u₁} [] {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.pathComposition_map (C : Type u₁) [] :
∀ {X Y : } (f : X Y),
@[simp]
theorem CategoryTheory.pathComposition_obj (C : Type u₁) [] (X : ) :
.obj X = X

Composition of paths as functor from the path category of a category to the category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.pathsHomRel (C : Type u₁) [] :

The canonical relation on the path category of a category: two paths are related if they compose to the same morphism.

Equations
• = (.map p = .map q)
Instances For
@[simp]
theorem CategoryTheory.toQuotientPaths_obj_as (C : Type u₁) [] (X : C) :
(.obj X).as = X
@[simp]
theorem CategoryTheory.toQuotientPaths_map (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), .map f =

The functor from a category to the canonical quotient of its path category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.quotientPathsTo_obj (C : Type u₁) [] :
.obj a = a.as
@[simp]
theorem CategoryTheory.quotientPathsTo_map (C : Type u₁) [] (hf : a b) :
.map hf = Quot.liftOn hf (fun (f : a.as b.as) => )

The functor from the canonical quotient of a path category of a category to the original category.

Equations
Instances For

The canonical quotient of the path category of a category is equivalent to the original category.

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