Kerodon

Proof of Proposition 1.5.7.3. Let $G$ be a directed graph and let $\operatorname{Path}[G]$ denote its path category. By definition, a morphism from $x \in \operatorname{Vert}(G)$ to $y \in \operatorname{Vert}(G)$ in the category $\operatorname{Path}[G]$ is given by a sequence of edges $\vec{e} = (e_ m, e_{m-1}, \ldots , e_1)$ satisfying

In this case, we will refer to $m$ as the length of the morphism $\vec{e}$ and write $m = \ell (\vec{e})$. If $\sigma : \Delta ^ n \rightarrow \operatorname{N}_{\bullet }(\operatorname{Path}[G])$ is an $n$-simplex given by a diagram

in $\operatorname{Path}[G]$, we define the length $\ell (\sigma )$ to be the sum $\ell ( \vec{e}_1 ) + \cdots + \ell ( \vec{e}_ n ) = \ell ( \vec{e}_ n \circ \cdots \circ \vec{e}_1 )$. For each positive integer $k$, let $\operatorname{N}_{\bullet }^{\leq k}( \operatorname{Path}[G] )$ denote the simplicial subset of $\operatorname{N}_{\bullet }( \operatorname{Path}[G] )$ consisting of those simplices having length $\leq k$. We then have inclusions

where $\operatorname{N}_{\bullet }^{\leq 1}( \operatorname{Path}[G] ) = G_{\bullet }$ and $\operatorname{N}_{\bullet }( \operatorname{Path}[G] ) = \bigcup \operatorname{N}_{\bullet }^{\leq k}( \operatorname{Path}[G] )$. Consequently, to show that the inclusion $G_{\bullet } \hookrightarrow \operatorname{N}_{\bullet }( \operatorname{Path}[G] )$ is inner anodyne, it will suffice to show that each of the inclusion maps $\operatorname{N}_{\bullet }^{\leq k}(\operatorname{Path}[G]) \hookrightarrow \operatorname{N}_{\bullet }^{\leq k+1}(\operatorname{Path}[G] )$ is inner anodyne.

We henceforth regard the integer $k \geq 1$ as fixed. Let $\sigma : \Delta ^ n \rightarrow \operatorname{N}_{\bullet }(\operatorname{Path}[G])$ be an $n$-simplex of $\operatorname{N}_{\bullet }( \operatorname{Path}[G] )$ having length $k+1$, corresponding to a diagram

as above. Note that $\sigma $ is nondegenerate if and only if each $\vec{e}_ i$ has positive length. We will say that $\sigma $ is normalized if it is nondegenerate and $\ell ( \vec{e}_1 ) = 1$. Let $S(n)$ be the collection of all normalized $n$-simplices of $\operatorname{N}_{\bullet }^{\leq k+1}( \operatorname{Path}[G] )$ having length $k+1$. We make the following observations:

$(i)$

If $\sigma $ belongs to $S(n)$, then the faces $d^{n}_0(\sigma )$ and $d^{n}_ n(\sigma )$ have length $\leq k$, and are therefore contained in $\operatorname{N}_{\bullet }^{\leq k}( \operatorname{Path}[G] )$.

$(ii)$

If $\sigma $ belongs to $S(n)$ and $1 < i < n$, then the face $d^{n}_ i(\sigma )$ is a normalized $(n-1)$-simplex of $\operatorname{N}_{\bullet }^{\leq k+1}( \operatorname{Path}[G] )$ of length $k+1$, and therefore belongs to $S(n-1)$.

$(iii)$

If $\sigma $ belongs to $S(n)$, then the face $d^{n}_1(\sigma )$ is not normalized. Moreover, the construction $\sigma \mapsto d^{n}_1(\sigma )$ induces a bijection from $S(n)$ to the collection of $(n-1)$-simplices of $\operatorname{N}_{\bullet }^{\leq k+1}( \operatorname{Path}[G] )$ which are nondegenerate, of length $k+1$, and not normalized.

For each $n \geq 1$, let $X(n)$ denote the simplicial subset of $\operatorname{N}_{\bullet }^{\leq k+1}( \operatorname{Path}[G] )$ given by the union of the $(n-1)$-skeleton $\operatorname{sk}_{n-1}( \operatorname{N}_{\bullet }^{\leq k+1}( \operatorname{Path}[G] ))$, the simplicial set $\operatorname{N}_{\bullet }^{\leq k}( \operatorname{Path}[G] )$, and the collection of normalized $n$-simplices of $\operatorname{N}_{\bullet }^{\leq k+1}( \operatorname{Path}[G] )$. We have inclusions

where $\operatorname{N}_{\bullet }^{\leq k}( \operatorname{Path}[G] ) = X(1)$ and $\operatorname{N}_{\bullet }^{\leq k+1}( \operatorname{Path}[G] ) = \bigcup _{n} X(n)$. It will therefore suffice to show that the inclusion maps $X(n-1) \hookrightarrow X(n)$ are inner anodyne for $n \geq 2$. We conclude by observing that $(i)$, $(ii)$, and $(iii)$ guarantee the existence of a pushout diagram of simplicial sets