Lemma 4.6.6.7 (04J4)

Lemma 4.6.6.7. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f_{+}: K_{+} \rightarrow \operatorname{\mathcal{C}}$ be a diagram. Then, for every simplicial set $K$, the comparison map

\[ \theta : \operatorname{Fun}(K, \operatorname{\mathcal{C}}_{ /f_{+} } ) \rightarrow \operatorname{Fun}( K \star K_{+}, \operatorname{\mathcal{C}}) \times _{ K_{+}, \operatorname{\mathcal{C}}) } \{ f_{+} \} \]

of Construction 4.6.6.4 is an equivalence of $\infty $-categories.

Proof. Let $c: K \diamond K_{+} \rightarrow K \star K_{+}$ be as in Notation 4.5.8.3. We then have a commutative diagram

\[ \xymatrix { \operatorname{Fun}( K \star K_{+}, \operatorname{\mathcal{C}}) \ar [r]^{ \circ c} \ar [d] & \operatorname{Fun}( K \diamond K_{+}, \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}( K_{+}, \operatorname{\mathcal{C}}) \ar@ {=}[r] & \operatorname{Fun}( K_{+}, \operatorname{\mathcal{C}}) } \]

where the vertical maps are isofibrations (Corollary 4.4.5.3). Since $c$ is a categorical equivalence of simplicial sets (Theorem 4.5.8.8), the upper horizontal map is an equivalence of $\infty $-categories. Applying Corollary 4.5.2.32, we conclude that composition with $c$ induces an equivalence of $\infty $-categories

\begin{eqnarray*} \operatorname{Fun}( K \star K_{+}, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(K_{+}, \operatorname{\mathcal{C}}) } \{ f_{+} \} & \xrightarrow {\theta '} & \operatorname{Fun}( K \diamond K_{+}, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(K_{+}, \operatorname{\mathcal{C}}) } \{ f_{+} \} \\ & \simeq & \operatorname{Fun}( K, \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K_{+}, \operatorname{\mathcal{C}}) } \{ f_{+} \} ). \end{eqnarray*}

It will therefore suffice to show that $\theta ' \circ \theta $ is an equivalence of $\infty $-categories. We conclude by observing that $\theta ' \circ \theta $ is given by postcomposition with the slice diagonal $\operatorname{\mathcal{C}}_{ /f_{+} } \hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K_{+}, \operatorname{\mathcal{C}}) } \{ f_{+} \} $, which is an equivalence of $\infty $-categories by virtue of Theorem 4.6.4.17. $\square$