Kerodon

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

Corollary 4.6.6.9. 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 inclusion of simplicial sets $A \hookrightarrow B$, the diagram of $\infty $-categories

4.59
\begin{equation} \begin{gathered}\label{equation:double-slice-consequence} \xymatrix { \operatorname{Fun}(B, \operatorname{\mathcal{C}}_{ f_{-} / \, / f_{+} }) \ar [r] \ar [d] & \operatorname{Fun}( K_{-} \star B \star K_{+},\operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}(A, \operatorname{\mathcal{C}}_{ f_{-} / \, / f_{+}} ) \ar [r] & \operatorname{Fun}( K_{-} \star A \star K_{+}, \operatorname{\mathcal{C}}) } \end{gathered} \end{equation}

is a categorical pullback square.

Proof. We can identify (4.59) with the upper half of a commutative diagram

\[ \xymatrix { \operatorname{Fun}(B, \operatorname{\mathcal{C}}_{ f_{-} / \, / f_{+} }) \ar [r] \ar [d] & \operatorname{Fun}( K_{-} \star B \star K_{+},\operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}(A, \operatorname{\mathcal{C}}_{ f_{-} / \, / f_{+}} ) \ar [r] \ar [d] & \operatorname{Fun}( K_{-} \star A \star K_{+}, \operatorname{\mathcal{C}}) \ar [d] \\ \{ f_{\pm } \} \ar [r] & \operatorname{Fun}( K_{-} \star K_{+}, \operatorname{\mathcal{C}}). } \]

By virtue of Proposition 4.5.2.18, it will suffice to show that the lower half and outer rectangle of the diagram are categorical pullback squares, which follows from Theorem 4.6.6.5. $\square$