The category paths on a quiver. #
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.
A type synonym for the category of paths in a quiver.
Equations
Instances for category_theory.paths
Equations
- category_theory.paths.inhabited V = {default := inhabited.default _inst_1}
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' := _}
The inclusion of a quiver V
into its path category, as a prefunctor.
Two functors out of a path category are equal when they agree on singleton paths.
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
- category_theory.path_composition C = {obj := λ (X : category_theory.paths C), X, map := λ (X Y : category_theory.paths C) (f : X ⟶ Y), category_theory.compose_path f, map_id' := _, map_comp' := _}
The canonical relation on the path category of a category: two paths are related if they compose to the same morphism.
Equations
- category_theory.paths_hom_rel C = λ (X Y : category_theory.paths C) (p q : X ⟶ Y), (category_theory.path_composition C).map p = (category_theory.path_composition C).map q
The functor from a category to the canonical quotient of its path category.
Equations
- category_theory.to_quotient_paths C = {obj := λ (X : C), {as := X}, map := λ (X Y : C) (f : X ⟶ Y), quot.mk (category_theory.quotient.comp_closure (category_theory.paths_hom_rel C)) f.to_path, map_id' := _, map_comp' := _}
The functor from the canonical quotient of a path category of a category to the original category.
The canonical quotient of the path category of a category is equivalent to the original category.
Equations
- category_theory.quotient_paths_equiv C = {functor := category_theory.quotient_paths_to C _inst_1, inverse := category_theory.to_quotient_paths C _inst_1, unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.quotient (category_theory.paths_hom_rel C)), X.cases_on (λ (X : category_theory.paths C), category_theory.iso.refl ((𝟭 (category_theory.quotient (category_theory.paths_hom_rel C))).obj {as := X}))) _, counit_iso := category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl ((category_theory.to_quotient_paths C ⋙ category_theory.quotient_paths_to C).obj X)) _, functor_unit_iso_comp' := _}