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.

source
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
source
@[protected, instance]
def category_theory.paths.inhabited (V : Type u₁) [inhabited V] :
inhabited (category_theory.paths V)
Equations
source
@[protected, instance]
def category_theory.paths.category_paths (V : Type u₁) [quiver V] :
category_theory.category (category_theory.paths V)
Equations
source
@[simp]
theorem category_theory.paths.of_map {V : Type u₁} [quiver V] (X Y : V) (f : X ⟶ Y) :
category_theory.paths.of.map f = f.to_path
source
@[simp]
theorem category_theory.paths.of_obj {V : Type u₁} [quiver V] (X : V) :
category_theory.paths.of.obj X = X
source
def category_theory.paths.of {V : Type u₁} [quiver V] :
V ⥤q category_theory.paths V

The inclusion of a quiver V into its path category, as a prefunctor.

Equations
source
def category_theory.paths.lift {V : Type u₁} [quiver V] {C : Type u_1} [category_theory.category C] (φ : V ⥤q C) :
category_theory.paths V ⥤ C

Any prefunctor from V lifts to a functor from paths V

Equations
source
@[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) :
(category_theory.paths.lift φ).map quiver.path.nil = 𝟙 (φ.obj X)
source
@[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) :
(category_theory.paths.lift φ).map (p.cons f) = (category_theory.paths.lift φ).map p ≫ φ.map f
source
@[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) :
(category_theory.paths.lift φ).map f.to_path = φ.map f
source
theorem category_theory.paths.lift_spec {V : Type u₁} [quiver V] {C : Type u_1} [category_theory.category C] (φ : V ⥤q C) :
category_theory.paths.of ⋙q (category_theory.paths.lift φ).to_prefunctor = φ
source
theorem category_theory.paths.lift_unique {V : Type u₁} [quiver V] {C : Type u_1} [category_theory.category C] (φ : V ⥤q C) (Φ : category_theory.paths V ⥤ C) (hΦ : category_theory.paths.of ⋙q Φ.to_prefunctor = φ) :
Φ = category_theory.paths.lift φ
source
@[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.

source
@[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)
source
@[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
source
@[simp]
theorem category_theory.compose_path_to_path {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :
category_theory.compose_path f.to_path = f
source
@[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) :
category_theory.compose_path (f.comp g) = category_theory.compose_path f ≫ category_theory.compose_path g
source
@[simp]
theorem category_theory.compose_path_id {C : Type u₁} [category_theory.category C] {X : category_theory.paths C} :
category_theory.compose_path (𝟙 X) = 𝟙 X
source
@[simp]
theorem category_theory.compose_path_comp' {C : Type u₁} [category_theory.category C] {X Y Z : category_theory.paths C} (f : X ⟶ Y) (g : Y ⟶ Z) :
category_theory.compose_path (f ≫ g) = category_theory.compose_path f ≫ category_theory.compose_path g
source
@[simp]
theorem category_theory.path_composition_obj (C : Type u₁) [category_theory.category C] (X : category_theory.paths C) :
(category_theory.path_composition C).obj X = X
source
@[simp]
theorem category_theory.path_composition_map (C : Type u₁) [category_theory.category C] (X Y : category_theory.paths C) (f : X ⟶ Y) :
(category_theory.path_composition C).map f = category_theory.compose_path f
source
def category_theory.path_composition (C : Type u₁) [category_theory.category C] :
category_theory.paths C ⥤ C

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

Equations
source
@[simp]
def category_theory.paths_hom_rel (C : Type u₁) [category_theory.category C] :
hom_rel (category_theory.paths C)

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

Equations
source
@[simp]
theorem category_theory.to_quotient_paths_map (C : Type u₁) [category_theory.category C] (X Y : C) (f : X ⟶ Y) :
(category_theory.to_quotient_paths C).map f = quot.mk (category_theory.quotient.comp_closure (category_theory.paths_hom_rel C)) f.to_path
source
@[simp]
theorem category_theory.to_quotient_paths_obj_as (C : Type u₁) [category_theory.category C] (X : C) :
((category_theory.to_quotient_paths C).obj X).as = X
source
def category_theory.to_quotient_paths (C : Type u₁) [category_theory.category C] :
C ⥤ category_theory.quotient (category_theory.paths_hom_rel C)

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

Equations
source
def category_theory.quotient_paths_to (C : Type u₁) [category_theory.category C] :
category_theory.quotient (category_theory.paths_hom_rel C) ⥤ C

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

Equations
source
@[simp]
theorem category_theory.quotient_paths_to_map (C : Type u₁) [category_theory.category C] (a b : category_theory.quotient (category_theory.paths_hom_rel C)) (hf : a ⟶ b) :
(category_theory.quotient_paths_to C).map hf = quot.lift_on hf (category_theory.path_composition C).map _
source
@[simp]
theorem category_theory.quotient_paths_to_obj (C : Type u₁) [category_theory.category C] (a : category_theory.quotient (category_theory.paths_hom_rel C)) :
(category_theory.quotient_paths_to C).obj a = a.as
source
def category_theory.quotient_paths_equiv (C : Type u₁) [category_theory.category C] :
category_theory.quotient (category_theory.paths_hom_rel C) ≌ C

The canonical quotient of the path category of a category is equivalent to the original category.

Equations