Kerodon

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

Proposition 4.5.5.18. Let $q: X \rightarrow S$ be an isofibration of simplicial sets and let $i: A \hookrightarrow B$ be a monomorphism of simplicial sets. If $i$ is a categorical equivalence, then the restriction map

\[ q': \operatorname{Fun}(B,X) \rightarrow \operatorname{Fun}(A,X) \times _{ \operatorname{Fun}(A,S) } \operatorname{Fun}(B,S) \]

is a trivial Kan fibration.

Proof. Let $B'$ be a simplicial set and let $A' \subseteq B'$ be a simplicial subset. We wish to show that every lifting problem

\[ \xymatrix@C =50pt{ A' \ar [d] \ar [r] & \operatorname{Fun}(B,X) \ar [d]^{q'} \\ B' \ar [r] \ar@ {-->}[ur] & \operatorname{Fun}(A,X) \times _{ \operatorname{Fun}(A,S) } \operatorname{Fun}(B,S) } \]

admits a solution. Unwinding the definitions, we are reduced to the problem of solving an associated lifting problem

\[ \xymatrix@C =50pt{ (A \times B') \coprod _{ (A \times A') } (B \times A') \ar [d] \ar [r] & X \ar [d]^{q} \\ B \times B' \ar [r] \ar@ {-->}[ur] & S. } \]

The left vertical map in this diagram is a categorical equivalence by virtue of Corollary 4.5.4.15, so the existence of the desired solution follows from our assumption that $q$ is an isofibration. $\square$