Kerodon

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

Corollary 5.1.4.22. Suppose we are given a commutative diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ X' \ar [dr]^{q'} \ar [rr]^{u} & & X \ar [dl]_{q} \\ & S & } \]

where $q$ and $q'$ are cartesian fibrations and the morphism $u$ carries $q'$-cartesian edges of $X'$ to $q$-cartesian edges of $X$. Let $f: K \rightarrow X$ be a morphism of simplicial sets. Then $q'$ induces a cartesian fibration $\widetilde{q}': X' \times _{X} X_{f/} \rightarrow S_{ (q \circ f)/ }$. Moreover, an edge of $X' \times _{X} X_{f/}$ is $\widetilde{q}'$-cartesian if and only if its image in $X'$ is $q'$-cartesian.

Proof. Let $\widetilde{u}: X' \times _{S} S_{ (q \circ f) / } \rightarrow X \times _{S} S_{ (q \circ f) /}$ denote the pullback of $u$, let $\widetilde{q}: X \times _{S} S_{ (q \circ f) /} \rightarrow S_{ (q \circ f) / }$ be given by projection onto the second factor, and let $v: X_{ f/} \rightarrow X \times _{S} S_{ (q \circ f)/ }$ be the left fibration of Proposition 4.3.6.8. Note that $\widetilde{q}$ is a pullback of $q$, and therefore a cartesian fibration (Remark 5.1.4.6). Moreover, an edge of $X \times _{S} S_{ (q \circ f) /}$ is $\widetilde{q}$-cartesian if and only if its image in $X$ is $q$-cartesian. Similarly, the composite map $\widetilde{q} \circ \widetilde{u}$ is a pullback of $q'$. It follows that $\widetilde{q} \circ \widetilde{u}$ is a cartesian fibration, and that an edge of $X' \times _{S} S_{ (q \circ f) / }$ is $(\widetilde{q} \circ \widetilde{u})$-cartesian if and only if its image in $X'$ is $q'$-cartesian. Applying Proposition 5.1.4.20, we deduce that the composition $\widetilde{q} \circ v$ is a cartesian fibration, and that an edge of $X_{ f/}$ is $(\widetilde{q} \circ v)$-cartesian if and only if its image in $X$ is $q$-cartesian. The desired result now follows by applying Proposition 5.1.4.21 to the diagram

\[ \xymatrix@R =50pt@C=50pt{ X' \times _{S} S_{ (q \circ f)/} \ar [r]^{\widetilde{u}} \ar [dr] & X \times _{S} S_{ (q \circ f)/ } \ar [d]^{\pi } & X_{ f/ } \ar [dl] \ar [l]_{v} \\ & S_{ (q\circ f)/ }. & } \]
$\square$