The category paths on a quiver. #
A type synonym for the category of paths in a quiver.
Equations
@[protected, instance]
Equations
- category_theory.paths.inhabited V = {default := default _inst_1}
@[protected, instance]
Equations
- category_theory.paths.category_paths V = {to_category_struct := {to_quiver := {hom := λ (X Y : V), quiver.path X Y}, id := λ (X : category_theory.paths V), quiver.path.nil, comp := λ (X Y Z : category_theory.paths V) (f : X ⟶ Y) (g : Y ⟶ Z), quiver.path.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
@[simp]
The inclusion of a quiver V into its path category, as a prefunctor.
@[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) :
@[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
@[simp]
theorem
category_theory.compose_path_comp
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : quiver.path X Y)
(g : quiver.path Y Z) :