Kerodon

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

Proposition 4.8.7.20. Let $m$ and $n$ be nonnegative integers and let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a categorically $(m+n)$-connective functor of $\infty$-categories. Let $B$ be a simplicial set of dimension $\leq m$, and let $A \subseteq B$ be a simplicial subset. Then the induced functor

$G: \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 categorically $n$-connective.

Proof. We proceed as in the proof of Proposition 3.5.2.11. Using Corollary 4.5.2.23 (and Corollary 4.5.2.30), we can reduce to the case where $F$ is an isofibration. In this case, $G$ is also an isofibration (Proposition 4.4.5.1). By virtue of Proposition 4.8.7.14, it will suffice to show that if $B'$ is a simplicial set of dimension $\leq n$ and $A' \subseteq B'$ is a simplicial subset, then every lifting problem

4.87
$$\begin{gathered}\label{equation:exponentiation-for-connectivity-categorical} \xymatrix@R =50pt@C=50pt{ A' \ar [r] \ar [d] & \operatorname{Fun}( B, \operatorname{\mathcal{C}}) \ar [d]^{G} \\ B' \ar [r] \ar@ {-->}[ur] & \operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}( A, \operatorname{\mathcal{D}}) } \operatorname{Fun}( B, \operatorname{\mathcal{D}}) } \end{gathered}$$

admits a solution. Unwinding the definitions, we can rewrite (4.87) as a lifting problem

$\xymatrix@R =50pt@C=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 [r] \ar@ {-->}[ur] & \operatorname{\mathcal{D}}. }$

Since the simplicial set $B \times B'$ has dimension $\leq m+n$ (Proposition 1.1.3.6), the existence of a solution follows from our assumption that $F$ is categorically $(m+n)$-connective (Proposition 4.8.7.14). $\square$