mathlib documentation

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
@[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) :

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} [category_theory.category C] {F G : category_theory.paths V C} (h_obj : F.obj = G.obj) (h : ∀ (a b : V) (e : a b), F.map e.to_path = category_theory.eq_to_hom _ G.map e.to_path category_theory.eq_to_hom _) :
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 : prefunctor V 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₁} [category_theory.category C] {X Y : C} (p : quiver.path X Y) :
X Y

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

Equations