Kerodon

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

Corollary 4.6.7.27. Let $\operatorname{\mathcal{C}}$ be a simplicial category containing a pair of objects $X$ and $Y$, and assume that the simplicial set $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)_{\bullet }$ is an $\infty $-category. Let $K$ be another simplicial set, and suppose we are given a pair of morphisms $f_0, f_1: K \rightarrow \operatorname{Hom}^{\mathrm{L}}_{ \operatorname{N}_{\bullet }^{\operatorname{hc}}(\operatorname{\mathcal{C}}) }(X,Y)$, which correspond (under the bijection of Corollary 4.6.7.17) to diagrams $f'_0,f'_1: \Phi (K) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)_{\bullet }$. The following conditions are equivalent:

$(1)$

The diagrams $f_0$ and $f_1$ are isomorphic when regarded as objects of the $\infty $-category $\operatorname{Fun}(K, \operatorname{Hom}^{\mathrm{L}}_{ \operatorname{N}_{\bullet }^{\operatorname{hc}}(\operatorname{\mathcal{C}}) }(X,Y) )$.

$(2)$

The diagrams $f'_0$ and $f'_1$ are isomorphic when regarded as objects of the $\infty $-category $\operatorname{Fun}( \Phi (K), \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)_{\bullet } )$.

Proof. Choose a categorical mapping cylinder

\[ K \coprod K \xrightarrow { (s_0, s_1) } \overline{K} \xrightarrow {\pi } K \]

for the simplicial set $K$ (Definition 4.6.3.3). Using Remark 4.6.7.15, Corollary 4.6.7.22, and Corollary 4.6.7.25, we conclude that the induced diagram

\[ \Phi (K) \coprod \Phi (K) \xrightarrow { ( \Phi (s_0), \Phi (s_1) ) } \Phi ( \overline{K} ) \xrightarrow { \Phi (\pi ) } \Phi (K) \]

exhibits $\Phi ( \overline{K} )$ as a categorical mapping cylinder of $K$. Using Corollary 4.6.3.7, we see that $(1)$ and $(2)$ are equivalent to the following:

$(1')$

There exists a diagram $\overline{f}: \overline{K} \rightarrow \operatorname{Hom}^{\mathrm{L}}_{ \operatorname{N}_{\bullet }^{\operatorname{hc}}(\operatorname{\mathcal{C}}) }(X,Y)$ satisfying $f_0 = \overline{f} \circ s_0$ and $f_1 = \overline{f} \circ s_1$.

$(2')$

There exists a diagram $\overline{f}': \Phi ( \overline{K} ) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)_{\bullet }$ satisfying $f'_0 = \overline{f}' \circ \Phi (s_0)$ and $f'_1 = \overline{f}' \circ \Phi (s_1)$.

The equivalence of $(1')$ and $(2')$ follows from Corollary 4.6.7.17. $\square$