Documentation

Mathlib.CategoryTheory.PathCategory

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
Instances For
    @[simp]
    theorem CategoryTheory.Paths.of_map {V : Type u₁} [Quiver V] :
    ∀ {X Y : V} (f : X Y), CategoryTheory.Paths.of.map f = f.toPath
    @[simp]
    theorem CategoryTheory.Paths.of_obj {V : Type u₁} [Quiver V] (X : V) :
    CategoryTheory.Paths.of.obj X = X

    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) => f.toPath }
    Instances For

      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
        @[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) :
        @[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) :
        @[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 φ).map f.toPath = φ.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 = φ) :

        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) :
        F.mapPath (CategoryTheory.CategoryStruct.comp f g) = (F.mapPath f).comp (F.mapPath 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
        Instances For
          @[simp]

          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

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

            Equations
            Instances For

              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

                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