mathlib3 documentation

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

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} [category_theory.category C] (φ : V ⥤q C) (X : V) :
@[simp]
theorem category_theory.paths.lift_cons {V : Type u₁} [quiver V] {C : Type u_1} [category_theory.category C] (φ : V ⥤q C) {X Y Z : V} (p : quiver.path X Y) (f : Y Z) :
@[simp]
theorem category_theory.paths.lift_to_path {V : Type u₁} [quiver V] {C : Type u_1} [category_theory.category C] (φ : V ⥤q C) {X Y : V} (f : X Y) :
@[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 : 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₁} [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

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

Equations
@[simp]

The canonical relation on the path category of a category: two paths are related if they compose to the same morphism.

Equations

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

Equations