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.

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

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

Equations

• CategoryTheory.Paths V = V

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

Equations

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

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

Equations

• CategoryTheory.Paths.categoryPaths V = CategoryTheory.Category.mk

@[simp]

theorem CategoryTheory.Paths.of_map {V : Type u₁} [Quiver V] : ∀ {X Y : V} (f : X ⟶ Y), CategoryTheory.Paths.of.map f = Quiver.Hom.toPath f

@[simp]

theorem CategoryTheory.Paths.of_obj {V : Type u₁} [Quiver V] (X : V) : CategoryTheory.Paths.of.obj X = X

def CategoryTheory.Paths.of {V : Type u₁} [Quiver V] : V ⥤q CategoryTheory.Paths V

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

Equations

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

def CategoryTheory.Paths.lift {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (φ : V ⥤q C) : CategoryTheory.Functor (CategoryTheory.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.

@[simp]

theorem CategoryTheory.Paths.lift_nil {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (φ : V ⥤q C) (X : V) : (CategoryTheory.Paths.lift φ).toPrefunctor.map Quiver.Path.nil = CategoryTheory.CategoryStruct.id (φ.obj X)

@[simp]

theorem CategoryTheory.Paths.lift_cons {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (φ : V ⥤q C) {X : V} {Y : V} {Z : V} (p : Quiver.Path X Y) (f : Y ⟶ Z) : (CategoryTheory.Paths.lift φ).toPrefunctor.map (Quiver.Path.cons p f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.lift φ).toPrefunctor.map p) (φ.map f)

@[simp]

theorem CategoryTheory.Paths.lift_toPath {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (φ : V ⥤q C) {X : V} {Y : V} (f : X ⟶ Y) : (CategoryTheory.Paths.lift φ).toPrefunctor.map (Quiver.Hom.toPath f) = φ.map f

theorem CategoryTheory.Paths.lift_spec {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (φ : V ⥤q C) : CategoryTheory.Paths.of ⋙q (CategoryTheory.Paths.lift φ).toPrefunctor = φ

theorem CategoryTheory.Paths.lift_unique {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (φ : V ⥤q C) (Φ : CategoryTheory.Functor (CategoryTheory.Paths V) C) (hΦ : CategoryTheory.Paths.of ⋙q Φ.toPrefunctor = φ) : Φ = CategoryTheory.Paths.lift φ

theorem CategoryTheory.Paths.ext_functor {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.Functor (CategoryTheory.Paths V) C} {G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (h_obj : F.obj = G.obj) (h : ∀ (a b : V) (e : a ⟶ b), F.toPrefunctor.map (Quiver.Hom.toPath e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.toPrefunctor.obj a = G.toPrefunctor.obj a)) (CategoryTheory.CategoryStruct.comp (G.toPrefunctor.map (Quiver.Hom.toPath e)) (CategoryTheory.eqToHom (_ : G.toPrefunctor.obj b = F.toPrefunctor.obj b)))) : F = G

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

@[simp]

theorem CategoryTheory.Prefunctor.mapPath_comp' (V : Type u₁) [Quiver V] (W : Type u₂) [Quiver W] (F : V ⥤q W) {X : CategoryTheory.Paths V} {Y : CategoryTheory.Paths V} {Z : CategoryTheory.Paths V} (f : X ⟶ Y) (g : Y ⟶ Z) : Prefunctor.mapPath F (CategoryTheory.CategoryStruct.comp f g) = Quiver.Path.comp (Prefunctor.mapPath F f) (Prefunctor.mapPath F g)

def CategoryTheory.composePath {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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 (Quiver.Path.cons p e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e

@[simp]

theorem CategoryTheory.composePath_nil {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CategoryTheory.composePath Quiver.Path.nil = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.composePath_cons {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : Quiver.Path X Y) (e : Y ⟶ Z) : CategoryTheory.composePath (Quiver.Path.cons p e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e

@[simp]

theorem CategoryTheory.composePath_toPath {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.composePath (Quiver.Hom.toPath f) = f

@[simp]

theorem CategoryTheory.composePath_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : Quiver.Path X Y) (g : Quiver.Path Y Z) : CategoryTheory.composePath (Quiver.Path.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath f) (CategoryTheory.composePath g)

@[simp]

theorem CategoryTheory.composePath_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : CategoryTheory.Paths C} : CategoryTheory.composePath (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (id X)

@[simp]

theorem CategoryTheory.composePath_comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : CategoryTheory.Paths C} {Y : CategoryTheory.Paths C} {Z : CategoryTheory.Paths C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.composePath (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath f) (CategoryTheory.composePath g)

@[simp]

theorem CategoryTheory.pathComposition_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : CategoryTheory.Paths C} (f : X ⟶ Y), (CategoryTheory.pathComposition C).toPrefunctor.map f = CategoryTheory.composePath f

@[simp]

theorem CategoryTheory.pathComposition_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Paths C) : (CategoryTheory.pathComposition C).toPrefunctor.obj X = X

def CategoryTheory.pathComposition (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor (CategoryTheory.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.

def CategoryTheory.pathsHomRel (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : HomRel (CategoryTheory.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).toPrefunctor.map p = (CategoryTheory.pathComposition C).toPrefunctor.map q)

@[simp]

theorem CategoryTheory.toQuotientPaths_obj_as (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : ((CategoryTheory.toQuotientPaths C).toPrefunctor.obj X).as = X

@[simp]

theorem CategoryTheory.toQuotientPaths_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.toQuotientPaths C).toPrefunctor.map f = Quot.mk (CategoryTheory.Quotient.CompClosure (CategoryTheory.pathsHomRel C)) (Quiver.Hom.toPath f)

def CategoryTheory.toQuotientPaths (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor C (CategoryTheory.Quotient (CategoryTheory.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.

@[simp]

theorem CategoryTheory.quotientPathsTo_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (a : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)) : (CategoryTheory.quotientPathsTo C).toPrefunctor.obj a = a.as

@[simp]

theorem CategoryTheory.quotientPathsTo_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (a : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)) (b : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)) (hf : a ⟶ b) : (CategoryTheory.quotientPathsTo C).toPrefunctor.map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => CategoryTheory.composePath f) (_ : ∀ (a_1 b_1 : a.as ⟶ b.as), CategoryTheory.Quotient.CompClosure (CategoryTheory.pathsHomRel C) a_1 b_1 → (fun (f : a.as ⟶ b.as) => (CategoryTheory.pathComposition C).toPrefunctor.map f) a_1 = (fun (f : a.as ⟶ b.as) => (CategoryTheory.pathComposition C).toPrefunctor.map f) b_1)

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

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

Equations

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

def CategoryTheory.quotientPathsEquiv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Quotient (CategoryTheory.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.