# Documentation

Mathlib.CategoryTheory.PathCategory

# 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.

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

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

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

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 () = 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 () = φ.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 () = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.obj a = G.obj a)) (CategoryTheory.CategoryStruct.comp (G.map ()) (CategoryTheory.eqToHom (_ : G.obj b = F.obj b)))) :
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) :
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_obj (C : Type u₁) [] (X : ) :
().obj X = X
@[simp]
theorem CategoryTheory.pathComposition_map (C : Type u₁) [] :
∀ {X Y : } (f : X Y),

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

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.

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),

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

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 b : a.as b.as), CategoryTheory.Quotient.CompClosure (fun x x_1 p q => ) a b(fun f => ().map f) a = (fun f => ().map f) b)

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

Instances For

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

Instances For