CategoryTheory.Paths.ext_functor
theorem CategoryTheory.Paths.ext_functor :
∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} C]
{F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (h_obj : F.obj = G.obj),
(∀ (a b : V) (e : a ⟶ b),
F.map e.toPath =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (G.map e.toPath) (CategoryTheory.eqToHom ⋯))) →
F = G
This theorem, `CategoryTheory.Paths.ext_functor`, states that for any type `V` with a `Quiver` structure, and any category `C`, if we have two functors `F` and `G` from the path category of `V` to `C` that agree on the object mapping, then they are equal if for every pair of elements `a` and `b` in `V` and a morphism `e` from `a` to `b`, the image of the path corresponding to `e` under `F` is equal to the composition of the morphism from the identity of `a` to `G.obj` times the composition of the morphism from `G.map e.toPath` to the identity of `b`. In other words, it states a condition under which two functors from a path category to another category can be considered equal.
More concisely: Given two functors from the path category of a quiver to a category with identical object mappings, they are equal if their action on paths agrees via the composition with identity morphisms and the image of a morphism's path.
|
CategoryTheory.composePath_toPath
theorem CategoryTheory.composePath_toPath :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
CategoryTheory.composePath f.toPath = f
The theorem `CategoryTheory.composePath_toPath` states that for any given category `C` and any two objects `X` and `Y` in `C`, if there is a morphism `f` from `X` to `Y`, then converting this morphism to a path using `Quiver.Hom.toPath` and then composing this path using `CategoryTheory.composePath` will yield the original morphism `f`. Essentially, it asserts the equivalence between the morphism `f` and its corresponding path representation when composed back to a morphism.
More concisely: For any category C and objects X, Y with a morphism f : X -> Y, the composed path of f's path representation and the identity path at Y equals f itself. (CategoryTheory.composePath (Quiver.Hom.toPath f) (CategoryTheory.pathId Y) = f)
|