# mathlibdocumentation

category_theory.path_category

# The category paths on a quiver. #

def category_theory.paths (V : Type u₁) :
Type u₁

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

Equations
@[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_comp {C : Type u₁} {X Y Z : C} (f : Y) (g : Z) :