# Kerodon

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

Lemma 5.1.4.18. Let $q: X \rightarrow S$ be an inner fibration of simplicial sets, let $f: B \rightarrow X$ be a morphism of simplicial sets, let $A$ be a simplicial subset of $B$, and let

$q': X_{f/} \rightarrow X_{ f|_{A} / } \times _{ S_{ ( q \circ f|_{A} )/}} S_{ (q \circ f)/}$

be the induced map. Let $\overline{e}$ be an edge of the simplicial set $X_{f/}$, and let $e$ be its image in $X$. If $e$ is $q$-cartesian, then $\overline{e}$ is $q'$-cartesian.

Proof. Let $q'': X_{ f|_{A} / } \times _{ S_{ ( q \circ f|_{A} )/}} S_{ (q \circ f)/} \rightarrow S_{ (q \circ f)/ }$ be the projection map onto the second factor. Then $q''$ is a pullback of the map $u: X_{ f|_{A} / } \rightarrow S_{ ( q \circ f|_{A} )/}$, and is therefore an inner fibration (Corollary 4.3.6.10). By virtue of Corollary 5.1.1.14, the edge $\overline{e}$ is $(q'' \circ q')$-cartesian and the image of $\overline{e}$ in $X_{ f_{A}/}$ is $u$-cartesian. It follows from Remark 5.1.1.11 that $q'( \overline{e} )$ is $q''$-cartesian, so that $\overline{e}$ is $q'$-cartesian by virtue of Corollary 5.1.2.6. $\square$