# 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.

source
def CategoryTheory.Paths (V : Type u₁) :
Type u₁

A type synonym for the category of paths in a quiver.

Equations

- CategoryTheory.Paths V = V

Instances For

source
instance CategoryTheory.instInhabitedPaths (V : Type u₁) [Inhabited V] :
Inhabited (Paths V)
Equations

- CategoryTheory.instInhabitedPaths V = { default := default }

source
instance CategoryTheory.Paths.categoryPaths (V : Type u₁) [Quiver V] :
Category.{max u₁ v₁, u₁} (Paths V)
Equations

- One or more equations did not get rendered due to their size.

source
def CategoryTheory.Paths.of (V : Type u₁) [Quiver V] :
V ⥤q Paths V

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

Equations

- CategoryTheory.Paths.of V = { obj := fun (X : V) => X, map := fun {X Y : V} (f : X ⟶ Y) => f.toPath }

Instances For

source
@[simp]
theorem CategoryTheory.Paths.of_map (V : Type u₁) [Quiver V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) :
(of V).map f = f.toPath
source
@[simp]
theorem CategoryTheory.Paths.of_obj (V : Type u₁) [Quiver V] (X : V) :
(of V).obj X = X
source
theorem CategoryTheory.Paths.induction_fixed_source {V : Type u₁} [Quiver V] {a : Paths V} (P : {b : Paths V} → (a ⟶ b) → Prop) (id : P (CategoryStruct.id a)) (comp : ∀ {u v : V} (p : a ⟶ (of V).obj u) (q : u ⟶ v), P p → P (CategoryStruct.comp p ((of V).map q))) {b : Paths V} (f : a ⟶ b) :
P f

To prove a property on morphisms of a path category with given source `a`, it suffices to prove it for the identity and prove that the property is preserved under composition on the right with length 1 paths.

source
theorem CategoryTheory.Paths.induction_fixed_target {V : Type u₁} [Quiver V] {b : Paths V} (P : {a : Paths V} → (a ⟶ b) → Prop) (id : P (CategoryStruct.id b)) (comp : ∀ {u v : V} (p : (of V).obj v ⟶ b) (q : u ⟶ v), P p → P (CategoryStruct.comp ((of V).map q) p)) {a : Paths V} (f : a ⟶ b) :
P f

To prove a property on morphisms of a path category with given target `b`, it suffices to prove it for the identity and prove that the property is preserved under composition on the left with length 1 paths.

source
theorem CategoryTheory.Paths.induction {V : Type u₁} [Quiver V] (P : {a b : Paths V} → (a ⟶ b) → Prop) (id : ∀ {v : V}, P (CategoryStruct.id ((of V).obj v))) (comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (CategoryStruct.comp p ((of V).map q))) {a b : Paths V} (f : a ⟶ b) :
P f

To prove a property on morphisms of a path category, it suffices to prove it for the identity and prove that the property is preserved under composition on the right with length 1 paths.

source
theorem CategoryTheory.Paths.induction' {V : Type u₁} [Quiver V] (P : {a b : Paths V} → (a ⟶ b) → Prop) (id : ∀ {v : V}, P (CategoryStruct.id ((of V).obj v))) (comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P (CategoryStruct.comp ((of V).map p) q)) {a b : Paths V} (f : a ⟶ b) :
P f

To prove a property on morphisms of a path category, it suffices to prove it for the identity and prove that the property is preserved under composition on the left with length 1 paths.

source
def CategoryTheory.Paths.lift {V : Type u₁} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] (φ : V ⥤q C) :
Functor (Paths V) C

Any prefunctor from `V` lifts to a functor from `paths V`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.Paths.lift_nil {V : Type u₁} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] (φ : V ⥤q C) (X : V) :
(lift φ).map Quiver.Path.nil = CategoryStruct.id (φ.obj X)
source
@[simp]
theorem CategoryTheory.Paths.lift_cons {V : Type u₁} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] (φ : V ⥤q C) {X Y Z : V} (p : Quiver.Path X Y) (f : Y ⟶ Z) :
(lift φ).map (p.cons f) = CategoryStruct.comp ((lift φ).map p) (φ.map f)
source
@[simp]
theorem CategoryTheory.Paths.lift_toPath {V : Type u₁} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] (φ : V ⥤q C) {X Y : V} (f : X ⟶ Y) :
(lift φ).map f.toPath = φ.map f
source
theorem CategoryTheory.Paths.lift_spec {V : Type u₁} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] (φ : V ⥤q C) :
of V ⋙q (lift φ).toPrefunctor = φ
source
theorem CategoryTheory.Paths.lift_unique {V : Type u₁} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] (φ : V ⥤q C) (Φ : Functor (Paths V) C) (hΦ : of V ⋙q Φ.toPrefunctor = φ) :
Φ = lift φ
source
theorem CategoryTheory.Paths.ext_functor {V : Type u₁} [Quiver V] {C : Type u_1} [Category.{u_2, u_1} C] {F G : Functor (Paths V) C} (h_obj : F.obj = G.obj) (h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map e.toPath) (eqToHom ⋯))) :
F = G

Two functors out of a path category are equal when they agree on singleton paths.

source
@[simp]
theorem CategoryTheory.Prefunctor.mapPath_comp' (V : Type u₁) [Quiver V] (W : Type u₂) [Quiver W] (F : V ⥤q W) {X Y Z : Paths V} (f : X ⟶ Y) (g : Y ⟶ Z) :
F.mapPath (CategoryStruct.comp f g) = (F.mapPath f).comp (F.mapPath g)
source
def CategoryTheory.composePath {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} :
Quiver.Path X Y → (X ⟶ Y)

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

Equations

- CategoryTheory.composePath Quiver.Path.nil = CategoryTheory.CategoryStruct.id X
- CategoryTheory.composePath (p.cons e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e

Instances For

source
theorem CategoryTheory.composePath_nil {C : Type u₁} [Category.{v₁, u₁} C] {X : C} :
composePath Quiver.Path.nil = CategoryStruct.id X
source
theorem CategoryTheory.composePath_cons {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : Quiver.Path X Y) (e : Y ⟶ Z) :
composePath (p.cons e) = CategoryStruct.comp (composePath p) e
source
@[simp]
theorem CategoryTheory.composePath_toPath {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
composePath f.toPath = f
source
@[simp]
theorem CategoryTheory.composePath_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : Quiver.Path X Y) (g : Quiver.Path Y Z) :
composePath (f.comp g) = CategoryStruct.comp (composePath f) (composePath g)
source
@[simp]
theorem CategoryTheory.composePath_id {C : Type u₁} [Category.{v₁, u₁} C] {X : Paths C} :
composePath (CategoryStruct.id X) = CategoryStruct.id (have this := X; this)
source
@[simp]
theorem CategoryTheory.composePath_comp' {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Paths C} (f : X ⟶ Y) (g : Y ⟶ Z) :
composePath (CategoryStruct.comp f g) = CategoryStruct.comp (composePath f) (composePath g)
source
def CategoryTheory.pathComposition (C : Type u₁) [Category.{v₁, u₁} C] :
Functor (Paths C) C

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.pathComposition_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Paths C} (f : X✝ ⟶ Y✝) :
(pathComposition C).map f = composePath f
source
@[simp]
theorem CategoryTheory.pathComposition_obj (C : Type u₁) [Category.{v₁, u₁} C] (X : Paths C) :
(pathComposition C).obj X = X
source
def CategoryTheory.pathsHomRel (C : Type u₁) [Category.{v₁, u₁} C] :
HomRel (Paths C)

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

Equations

- CategoryTheory.pathsHomRel C p q = ((CategoryTheory.pathComposition C).map p = (CategoryTheory.pathComposition C).map q)

Instances For

source
def CategoryTheory.toQuotientPaths (C : Type u₁) [Category.{v₁, u₁} C] :
Functor C (Quotient (pathsHomRel C))

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.toQuotientPaths_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
(toQuotientPaths C).map f = Quot.mk (Quotient.CompClosure (pathsHomRel C)) f.toPath
source
@[simp]
theorem CategoryTheory.toQuotientPaths_obj_as (C : Type u₁) [Category.{v₁, u₁} C] (X : C) :
((toQuotientPaths C).obj X).as = X
source
def CategoryTheory.quotientPathsTo (C : Type u₁) [Category.{v₁, u₁} C] :
Functor (Quotient (pathsHomRel C)) C

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

Equations

- CategoryTheory.quotientPathsTo C = CategoryTheory.Quotient.lift (CategoryTheory.pathsHomRel C) (CategoryTheory.pathComposition C) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.quotientPathsTo_obj (C : Type u₁) [Category.{v₁, u₁} C] (a : Quotient (pathsHomRel C)) :
(quotientPathsTo C).obj a = a.as
source
@[simp]
theorem CategoryTheory.quotientPathsTo_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Quotient (pathsHomRel C)} (hf : X✝ ⟶ Y✝) :
(quotientPathsTo C).map hf = Quot.liftOn hf (fun (f : X✝.as ⟶ Y✝.as) => composePath f) ⋯
source
def CategoryTheory.quotientPathsEquiv (C : Type u₁) [Category.{v₁, u₁} C] :
Quotient (pathsHomRel C) ≌ C

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

Equations

- One or more equations did not get rendered due to their size.

Instances For