Kerodon

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

Proposition 4.2.3.1. Let $f: X_{} \rightarrow S_{}$ and $i: A_{} \hookrightarrow B_{}$ be morphisms of simplicial sets, where $i$ is a monomorphism, and let

$\rho : \operatorname{Fun}( B_{}, X_{} ) \rightarrow \operatorname{Fun}( B_{}, S_{} ) \times _{ \operatorname{Fun}( A_{}, S_{} )} \operatorname{Fun}( A_{}, X_{} )$

be the induced map. If $f$ is a left fibration, then $\rho$ is a left fibration. If $f$ is a right fibration, then $\rho$ is a right fibration.

Proof of Proposition 4.2.3.1. Let $f: X \rightarrow S$ be a left fibration of simplicial sets and let $i: A \hookrightarrow B$ be a monomorphism of simplicial sets. We wish to show that the restriction map

$\rho : \operatorname{Fun}( B_{}, X_{} ) \rightarrow \operatorname{Fun}( B_{}, S_{} ) \times _{ \operatorname{Fun}( A_{}, S_{} )} \operatorname{Fun}( A_{}, X_{} )$

is also a left fibration (the dual assertion about right fibrations follows by passing to opposite simplicial sets). By virtue of Proposition 4.2.2.5, this is equivalent to the assertion that every lifting problem

$\xymatrix@C =100pt{ A'_{} \ar [d]^{i'} \ar [r] & \operatorname{Fun}( B_{}, X_{} ) \ar [d]^{\rho } \\ B'_{} \ar@ {-->}[ur] \ar [r] & \operatorname{Fun}( B_{}, S_{} ) \times _{ \operatorname{Fun}( A_{}, S_{} )} \operatorname{Fun}( A_{}, X_{} ) }$

admits a solution, provided that $i'$ is left anodyne. Equivalently, we must show that every lifting problem

$\xymatrix@C =100pt{ (A_{} \times B'_{} ) \coprod _{ A_{} \times A'_{} } ( B_{} \times A'_{} ) \ar [r] \ar [d] & X_{} \ar [d]^{f} \\ B_{} \times B'_{} \ar [r] \ar@ {-->}[ur] & S_{} }$

admits a solution. This follows from Proposition 4.2.2.5, since the left vertical map is left anodyne (Proposition 4.2.3.3) and the right vertical map is a left fibration. $\square$