# Kerodon

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

Proposition 4.4.5.1. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty$-categories, let $B$ be a simplicial set, and let $A \subseteq B$ be a simplicial subset. Then the restriction 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 an isofibration of $\infty$-categories.

Proof of Proposition 4.4.5.1. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty$-categories, let $B$ be a simplicial set, and let $A \subseteq B$ be a simplicial subset. We wish to show that the restriction 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 an isofibration of $\infty$-categories. We first note that the projection map

$\operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{C}})$

is a pullback of the inner fibration $\operatorname{Fun}(B, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{D}})$ (see Corollary 4.1.4.2). Since $\operatorname{Fun}(A, \operatorname{\mathcal{C}})$ is an $\infty$-category (Theorem 1.4.3.7), it follows that $\operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}})$ is also an $\infty$-category (Remark 4.1.1.9). It follows from Proposition 4.1.4.1 that $F'$ is an inner fibration. It will therefore suffice to show that, for every object $Y \in \operatorname{Fun}(B,\operatorname{\mathcal{C}})$, every isomorphism $u: X \rightarrow F'(Y)$ in the $\infty$-category $\operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}})$ can be lifted to an isomorphism $\overline{u}: \overline{X} \rightarrow Y$ in the $\infty$-category $\operatorname{Fun}(B, \operatorname{\mathcal{C}})$. This follows immediately from Corollary 4.4.5.9. $\square$