Kerodon

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

Proposition 4.8.8.16. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of simplicial sets and let $n$ be an integer. Then, for every $n$-categorical inner fibration $\operatorname{\mathcal{D}}' \rightarrow \operatorname{\mathcal{D}}$, the comparison map of Remark 4.8.8.15 induces an isomorphism of simplicial sets

\[ \theta : \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}, \operatorname{\mathcal{D}}' ) \rightarrow \operatorname{Fun}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}' ). \]

Proof. We may assume without loss of generality that $n \geq 0$ (otherwise, the result follows immediately from the construction). For every morphism of simplicial sets $K \rightarrow \operatorname{\mathcal{D}}$, Remark 4.8.8.15 determines a comparison map

\[ \theta _{K}: \operatorname{Fun}_{/\operatorname{\mathcal{D}}}( K \times _{\operatorname{\mathcal{D}}} \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}, \operatorname{\mathcal{D}}' ) \rightarrow \operatorname{Fun}_{/\operatorname{\mathcal{D}}}( K \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}' ). \]

We will prove that each $\theta _{K}$ is an isomorphism of simplicial sets; Proposition 4.8.8.16 then follows by taking $K = \operatorname{\mathcal{D}}$. Note that the construction $K \mapsto \theta _{K}$ carries colimits (in the category of simplicial sets with a morphism to $\operatorname{\mathcal{D}}$) to limits (in the arrow category $\operatorname{Fun}( [1], \operatorname{Set_{\Delta }})$). By virtue of Remark 1.1.3.13, we can assume without loss of generality that $K$ is a standard simplex. Replacing $F$ by the projection map $K \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}\rightarrow K$ and $\operatorname{\mathcal{D}}'$ by the fiber product $K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}'$, we are reduced to proving Proposition 4.8.8.16 in the special case where $\operatorname{\mathcal{D}}$ is a standard simplex: in particular, it is an $(n,1)$-category. In this case, $\operatorname{\mathcal{D}}'$ is also an $(n,1)$-category (Proposition 4.8.6.31), and we can identify $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ with the homotopy $n$-category of $\operatorname{\mathcal{C}}$ (Example 4.8.8.11). Applying Proposition 4.8.4.7, we see that the horizontal maps in the commutative diagram

\[ \xymatrix@C =50pt@R=50pt{ \operatorname{Fun}( \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}, \operatorname{\mathcal{D}}' ) \ar [r] \ar [d] & \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}' ) \ar [d] \\ \operatorname{Fun}( \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}, \operatorname{\mathcal{D}}) \ar [r] & \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) } \]

are isomorphisms. The desired result now follows by passing to fibers of the vertical maps. $\square$