Kerodon

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

Corollary 4.8.6.20. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, let $B$ be a simplicial set, and let $A \subseteq B$ be a simplicial subset. If $F$ is essentially $n$-categorical, then the induced functor $F': \operatorname{Fun}(B, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}})$ is also essentially $n$-categorical.

Proof. If $n \leq -2$, then $F$ is an equivalence of $\infty $-categories; it then follows from Corollary 4.5.2.30 that $F'$ is also an equivalence of $\infty $-categories. We may therefore assume that $n \geq -1$. Using Proposition 3.1.7.1, we can reduce to the case where $F$ is an inner fibration, so that $F'$ is also an inner fibration (Proposition 4.1.4.1). By virtue of Proposition 4.8.6.19, it will suffice to show that for every simplicial set $B'$ and every simplicial subset $A' \subseteq B'$ which contains the $(n+1)$-skeleton of $B$, every lifting problem

4.84
\begin{equation} \begin{gathered}\label{equation:locally-truncated-exponentiation} \xymatrix@C =50pt@R=50pt{ A' \ar [r] \ar [d] & \operatorname{Fun}(B,\operatorname{\mathcal{C}}) \ar [d]^{F'} \\ B' \ar@ {-->}[ur] \ar [r] & \operatorname{Fun}(A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}}) } \end{gathered} \end{equation}

Unwinding the definitions, we can rewrite (4.84) as a lifting problem

\[ \xymatrix@C =50pt@R=50pt{ (A \times B') \coprod _{ (A \times A') } (B \times A') \ar [r] \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{F} \\ B \times B' \ar@ {-->}[ur] \ar [r] & \operatorname{\mathcal{D}}. } \]

The existence of a solution now follows from Proposition 4.8.6.19, since $F$ is essentially $n$-categorical and $(A \times B') \coprod _{ (A \times A') } (B \times A')$ contains the $(n+1)$-skeleton of $B \times B'$. $\square$