# mathlibdocumentation

category_theory.path_category

# 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 category_theory.paths (V : Type u₁) :
Type u₁

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

Equations
Instances for category_theory.paths
@[protected, instance]
def category_theory.paths.inhabited (V : Type u₁) [inhabited V] :
Equations
@[protected, instance]
def category_theory.paths.category_paths (V : Type u₁) [quiver V] :
Equations
@[simp]
theorem category_theory.paths.of_map {V : Type u₁} [quiver V] (X Y : V) (f : X Y) :
@[simp]
theorem category_theory.paths.of_obj {V : Type u₁} [quiver V] (X : V) :
def category_theory.paths.of {V : Type u₁} [quiver V] :

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

Equations
@[ext]
theorem category_theory.paths.ext_functor {V : Type u₁} [quiver V] {C : Type u_1} {F G : C} (h_obj : F.obj = G.obj) (h : ∀ (a b : V) (e : a b), ) :
F = G

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

@[simp]
theorem category_theory.prefunctor.map_path_comp' (V : Type u₁) [quiver V] (W : Type u₂) [quiver W] (F : W) {X Y Z : category_theory.paths V} (f : X Y) (g : Y Z) :
F.map_path (f g) = (F.map_path f).comp (F.map_path g)
@[simp]
def category_theory.compose_path {C : Type u₁} {X Y : C} (p : Y) :
X Y

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

Equations
@[simp]
theorem category_theory.compose_path_to_path {C : Type u₁} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.compose_path_comp {C : Type u₁} {X Y Z : C} (f : Y) (g : Z) :
@[simp]
theorem category_theory.compose_path_id {C : Type u₁} {X : category_theory.paths C} :
@[simp]
theorem category_theory.compose_path_comp' {C : Type u₁} {X Y Z : category_theory.paths C} (f : X Y) (g : Y Z) :
@[simp]
theorem category_theory.path_composition_obj (C : Type u₁) (X : category_theory.paths C) :
@[simp]
theorem category_theory.path_composition_map (C : Type u₁) (X Y : category_theory.paths C) (f : X Y) :
def category_theory.path_composition (C : Type u₁)  :

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

Equations
@[simp]
def category_theory.paths_hom_rel (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
• = λ (X Y : (p q : X Y),
@[simp]
theorem category_theory.to_quotient_paths_map (C : Type u₁) (X Y : C) (f : X Y) :
@[simp]
theorem category_theory.to_quotient_paths_obj_as (C : Type u₁) (X : C) :
.as = X
def category_theory.to_quotient_paths (C : Type u₁)  :

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

Equations
def category_theory.quotient_paths_to (C : Type u₁)  :

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

Equations
@[simp]
theorem category_theory.quotient_paths_to_map (C : Type u₁) (hf : a b) :
@[simp]
theorem category_theory.quotient_paths_to_obj (C : Type u₁)  :
def category_theory.quotient_paths_equiv (C : Type u₁)  :

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

Equations