Kerodon

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

Corollary 4.8.4.14. 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 $n$-faithful for some integer $n$, then the induced map $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 $n$-faithful. Moreover, if $A$ contains the $n$-skeleton of $B$, then $F'$ is an equivalence of $\infty $-categories.

Proof. If $n < 0$, then $F$ is an equivalence of $\infty $-categories (Theorem 4.8.4.1); it then follows from Corollary 4.5.3.34 that $F'$ is also an equivalence of $\infty $-categories. We may therefore assume that $n \geq 0$. Using Proposition 3.1.8.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.4.13, it will suffice to show that for every simplicial set $B'$ and every simplicial subset $A' \subseteq B'$ every lifting problem

4.85
\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}

admits a solution provided either that $A$ contains the $n$-skeleton of $B$ or $A'$ contains the $n$-skeleton of $B'$. Unwinding the definitions, we can rewrite (4.85) 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.4.13, since $F$ is $n$-faithful and $(A \times B') \coprod _{ (A \times A') } (B \times A')$ contains the $n$-skeleton of $B \times B'$. $\square$