# mathlib3documentation

category_theory.path_category

# The category paths on a quiver. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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]
Equations
@[protected, instance]
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
def category_theory.paths.lift {V : Type u₁} [quiver V] {C : Type u_1} (φ : V ⥤q C) :

Any prefunctor from V lifts to a functor from paths V

Equations
@[simp]
theorem category_theory.paths.lift_nil {V : Type u₁} [quiver V] {C : Type u_1} (φ : V ⥤q C) (X : V) :
= 𝟙 (φ.obj X)
@[simp]
theorem category_theory.paths.lift_cons {V : Type u₁} [quiver V] {C : Type u_1} (φ : V ⥤q C) {X Y Z : V} (p : Y) (f : Y Z) :
(p.cons f) = φ.map f
@[simp]
theorem category_theory.paths.lift_to_path {V : Type u₁} [quiver V] {C : Type u_1} (φ : V ⥤q C) {X Y : V} (f : X Y) :
= φ.map f
theorem category_theory.paths.lift_spec {V : Type u₁} [quiver V] {C : Type u_1} (φ : V ⥤q C) :
theorem category_theory.paths.lift_unique {V : Type u₁} [quiver V] {C : Type u_1} (φ : V ⥤q C) (Φ : C) (hΦ : = φ) :
@[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 : V ⥤q 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]
@[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_map (C : Type u₁) (X Y : category_theory.paths C) (f : X Y) :

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

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

Equations

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]

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

Equations