Kerodon

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

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

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

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

Proof of Theorem 4.6.6.5. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f_{\pm }: K_{-} \star K_{+} \rightarrow \operatorname{\mathcal{C}}$ be a diagram. Set $f_{-} = f_{\pm } |_{ K_{-} }$ and $f_{+} = f_{\pm } |_{ K_{+} }$, so that $f_{\pm }$ can be identified with a morphism $\widetilde{f}_{-}: K_{-} \rightarrow \operatorname{\mathcal{C}}_{ / f_{+} }$. We then have a commutative diagram of simplicial sets

\[ \xymatrix { \operatorname{Fun}(K, \operatorname{\mathcal{C}}_{ f_{-} / \, / f_{+} } ) \ar [r] \ar [d] & \operatorname{Fun}(K_{-} \star K, \operatorname{\mathcal{C}}_{ / f_{+} } ) \ar [r] \ar [d] & \operatorname{Fun}(K_{-} \star K \star K_{+}, \operatorname{\mathcal{C}}) \ar [d] \\ \{ \widetilde{f}_{-} \} \ar [r] & \operatorname{Fun}( K_{-}, \operatorname{\mathcal{C}}_{ / f_{+} } ) \ar [r] \ar [d] & \operatorname{Fun}( K_{-} \star K_{+} , \operatorname{\mathcal{C}}) \ar [d] \\ & \{ f_{+} \} \ar [r] & \operatorname{Fun}( K_{+}, \operatorname{\mathcal{C}}), } \]

where the vertical maps are isofibrations (Corollary 4.4.5.3). It follows from Lemma 4.6.6.7 (and Proposition 4.5.2.26) that the lower right square and the outer right rectangle are categorical pullback squares, so the upper right corner is also a categorical pullback square (Proposition 4.5.2.18). Similarly, the dual of Lemma 4.6.6.7 guarantees that the upper left corner is a categorical pullback square. Applying Proposition 4.5.2.18, we conclude that the outer rectangle on the top of the diagram is a categorical pullback square, which is a restatement of Theorem 4.6.6.5 (Proposition 4.5.2.26). $\square$