Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 1.3.7.5. Let $G$ be a directed graph. Then the map of simplicial sets $u: G_{\bullet } \rightarrow \operatorname{N}_{\bullet }(\operatorname{Path}[G] )$ exhibits $\operatorname{Path}[G]$ as the homotopy category of the simplicial set $G_{\bullet }$, in the sense of Definition 1.3.6.1. In other words, for every category $\operatorname{\mathcal{C}}$, the composite map

\[ \operatorname{Hom}_{\operatorname{Cat}}( \operatorname{Path}[G], \operatorname{\mathcal{C}}) \rightarrow \operatorname{Hom}_{ \operatorname{Set_{\Delta }}}( \operatorname{N}_{\bullet }( \operatorname{Path}[G] ), \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) ) \xrightarrow {\circ u} \operatorname{Hom}_{\operatorname{Set_{\Delta }}}(G_{\bullet }, \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})) \]

is a bijection.

Proof. Let $f: G_{\bullet } \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a morphism of simplicial sets. We wish to show that there is a unique functor $F: \operatorname{Path}[G] \rightarrow \operatorname{\mathcal{C}}$ for which the composite map

\[ G_{\bullet } \xrightarrow {u} \operatorname{N}_{\bullet }( \operatorname{Path}[G] ) \xrightarrow { \operatorname{N}_{\bullet }(F)} \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) \]

coincides with $f$. Unwinding the definitions, we see that this agreement imposes the following requirements on $F$:

$(a)$

For each vertex $v \in \operatorname{Vert}(G)$, we have $F(x) = f(x)$ (as objects of $\operatorname{\mathcal{C}}$).

$(b)$

For each edge $e \in \operatorname{Edge}(G)$ having $x = s(e)$ and target $y = t(e)$, the functor $F$ carries the path $(e)$ to the morphism $f(e): f(x) \rightarrow f(y)$ in $\operatorname{\mathcal{C}}$.

The existence and uniqueness of the functor $F$ is now clear: it is determined on objects by property $(a)$, and on morphisms by the formula

\[ F( e_ n, e_{n-1}, \cdots , e_1 ) = f(e_ n) \circ f(e_{n-1} ) \circ \cdots \circ f(e_1). \]
$\square$