English
There is an equivalence of categories between Functors(Paths V, C) and Prefunctors(V, C). The forward direction sends F to F.toPrefunctor after Paths.of V, and the inverse sends G to Cat.freeMap G composed with pathComposition C.
Русский
Существует эквиваленция категорий между Functors(Paths V, C) и Prefunctors(V, C). Прямое отображение отправляет F в F.toPrefunctor после Paths.of V, обратное — G в Cat.freeMap G затем pathComposition C.
LaTeX
$$$\mathrm{Fun}(\mathrm{Paths}(V), C) \simeq \mathrm{Prefunctor}(V, C)$$$
Lean4
/-- The universal property of the path category of a quiver. -/
def pathsEquiv {V : Type u} {C : Type u₁} [Quiver.{v + 1} V] [Category.{v₁} C] : (Paths V ⥤ C) ≃ V ⥤q C
where
toFun F := (Paths.of V).comp F.toPrefunctor
invFun G := Cat.freeMap G ⋙ pathComposition C
left_inv
F := by
dsimp
rw [Cat.freeMap_comp, Functor.assoc, pathComposition_naturality, ← Functor.assoc, freeMap_pathsOf_pathComposition,
Functor.id_comp]
right_inv
G := by
dsimp
rw [← Functor.toPrefunctor_comp, ← Prefunctor.comp_assoc, pathsOf_freeMap_toPrefunctor, Prefunctor.comp_assoc,
pathsOf_pathComposition_toPrefunctor, Prefunctor.comp_id]
