Kerodon

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

Lemma 4.6.4.21. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $F: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram indexed by a simplicial set $K$. Suppose we are given a pair of diagrams $e_0, e_1: J \rightarrow \operatorname{\mathcal{C}}_{/F}$ indexed by a simplicial set $J$, which we identify with diagrams $F_0, F_1: J \star K \rightarrow \operatorname{\mathcal{C}}$ satisfying $F_0|_{K} = F = F_{1}|_{K}$. The following conditions are equivalent:

$(1)$

The diagrams $e_0$ and $e_1$ are isomorphic when regarded as objects of the diagram $\infty $-category $\operatorname{Fun}(J, \operatorname{\mathcal{C}}_{/F} )$.

$(2)$

The diagrams $F_0$ and $F_1$ are isomorphic when regarded as objects of the $\infty $-category $\operatorname{Fun}_{ K / }(J \star K, \operatorname{\mathcal{C}})$.

Proof. Choose a categorical mapping cylinder

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

for the simplicial set $J$ (Definition 4.6.3.3). Using Corollary 4.5.8.9, we deduce that the resulting diagram

\[ (J \star K) \coprod _{K} (J \star K) \xrightarrow {(s'_0, s'_1)} \overline{J} \star K \xrightarrow {\pi '} J \star K \]

is a categorical mapping cylinder for the join $J \star K$ relative to $K$. Using the criterion of Corollary 4.6.3.11, we see that $(1)$ and $(2)$ can be reformulated as follows:

$(1')$

There exists a diagram $\overline{e}: \overline{J} \rightarrow \operatorname{\mathcal{C}}_{/F}$ satisfying $e_0 = \overline{e} \circ s_0$ and $e_1 = \overline{e} \circ s_1$.

$(2')$

There exists a diagram $\overline{F}': \overline{J} \star K \rightarrow \operatorname{\mathcal{C}}$ satisfying $F_0 = \overline{F} \circ s'_0$ and $F_1 = \overline{F} \circ s'_1$.

The equivalence of $(1')$ and $(2')$ follows immediately from the universal property of the slice $\infty $-category $\operatorname{\mathcal{C}}_{/F}$. $\square$