Kerodon

Proof of Theorem 2.4.4.10. Let $m$ be a nonnegative integer, which we regard as fixed throughout the proof. For each simplicial set $S$, let $G( S )$ denote the directed graph given by

where we regard each element

as an edge of $G(S)$ having source $\sigma (0) \in \operatorname{Vert}( G(S) )$ and target $\sigma (n) \in \operatorname{Vert}( G(S))$. Let $u_{S}: S \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Path}[ S ] )$ exhibit the simplicial category $\operatorname{Path}_{\bullet }[S]$ as a path category of $S$. Then $u_{S}$ induces a map of simplicial sets $G(S)_{\bullet } \rightarrow \operatorname{N}_{\bullet }( \operatorname{Path}[S]_{m} )$, which we can identify with a functor of ordinary categories $F_{S}: \operatorname{Path}[ G(S) ] \rightarrow \operatorname{Path}[ S ]_{m}$. Let us say that the simplicial set $S$ is good if $F_{S}$ is an isomorphism of categories. Theorem 2.4.4.10 is equivalent to the assertion that every simplicial set is good (for every choice of nonnegative integer $m$). We will prove this by verifying that the collection of good simplicial sets satisfies the hypotheses of Lemma 1.2.3.13:

• Suppose we are given a pushout diagram of simplicial sets $\sigma :$

  \[ \xymatrix@R =50pt@C=50pt{ S \ar [r] \ar [d] & T \ar [d] \\ S' \ar [r] & T', } \]

  where the horizontal maps are monomorphisms. Suppose that $S$, $T$, and $S'$ are good; we wish to show that $T'_{\bullet }$ is good. Note that the horizonal maps induce monomorphisms of directed graphs

  \[ G(S) \hookrightarrow G(T ) \quad \quad G(S' ) \hookrightarrow G(T'). \]

  Define subgraphs $G_0(S) \subseteq G(S )$ and $G_0( T) \subseteq G(T )$ by the formulae

  \[ \operatorname{Vert}( G_0(S ) ) = \operatorname{Vert}( G(S) ) = S_0 \quad \quad \operatorname{Vert}( G_0(T ) ) = \operatorname{Vert}( G(T) ) = T_0 \]
  \[ \operatorname{Edge}( G_0( S) ) = \emptyset \quad \quad \operatorname{Edge}( G_0( T ) ) = \operatorname{Edge}( G(T) ) \setminus \operatorname{Edge}( G( S) ). \]

  We then have a commutative diagram of categories

  \[ \xymatrix@R =50pt@C=50pt{ \operatorname{Path}[ G_0(S)] \ar [r] \ar [d] & \operatorname{Path}[ G_0(T) ] \ar [d] \\ \operatorname{Path}[ G( S' ) ] \ar [r] \ar [d]^{ F_{S'} } & \operatorname{Path}[ G( T' )] \ar [d]^{ F_{T'} } \\ \operatorname{Path}[ S' ]_{m} \ar [r] & \operatorname{Path}[ T' ]_{m}. } \]

  We wish to show that the functor $F_{T'}$ is an isomorphism of categories, and the map $F_{S' }$ is an isomorphism by assumption. It will therefore suffice to show that the lower square in this diagram is a pushout. Note that the upper square is a pushout (since it is obtained from a pushout diagram in the category of directed graphs by passing to path categories). We are therefore reduced to showing that the outer rectangle is a pushout. We can rewrite this as the outer rectangle in another commutative diagram of categories

  \[ \xymatrix@R =50pt@C=50pt{ \operatorname{Path}[ G_0(S)] \ar [r] \ar [d] & \operatorname{Path}[ G_0(T) ] \ar [d] \\ \operatorname{Path}[ G( S ) ] \ar [r] \ar [d]^{ F_{S} } & \operatorname{Path}[ G(T )] \ar [d]^{ F_{T} } \\ \operatorname{Path}[ S ]_{m} \ar [r] \ar [d] & \operatorname{Path}[ T ]_{m} \ar [d] \\ \operatorname{Path}[ S' ]_{m} \ar [r] & \operatorname{Path}[ T' ]_{m}. } \]

  We now conclude by observing that the upper square in this diagram is a pushout (because it is obtained from a pushout diagram of directed graphs by passing to path categories), the middle square is a pushout (since $F_{S}$ and $F_{T}$ are isomorphisms), and the lower square is a pushout (since the construction $X_{\bullet } \mapsto \operatorname{Path}[ X ]_{m}$ preserves colimits).

• Suppose we are given a sequence of monomorphisms of simplicial sets

  \[ S(0) \hookrightarrow S(1) \hookrightarrow S(2) \hookrightarrow \cdots \]

  with colimit $S$. Then the functor $F_{S}: \operatorname{Path}[ G(S) ] \rightarrow \operatorname{Path}[ S ]_{m}$ can be written as a filtered colimit of functors $F_{S(i)}: \operatorname{Path}[ G(S(i))] \rightarrow \operatorname{Path}[ S(i) ]_{m}$. Consequently, if each $S(i)$ is good, then $S$ is good.

• Let $S$ be a simplicial set which can be written as a coproduct $\coprod _{i \in I} \Delta ^ n$; we must show that $S$ is good. Without loss of generality, we may assume that $I$ is a singleton, so that $S = \Delta ^ n$. In this case, Example 2.4.4.6 supplies an equivalence of simplicial categories $\operatorname{Path}[S]_{\bullet } \simeq \operatorname{Path}[n]_{\bullet }$. The desired result now follows from Lemma 2.4.4.16.