# Kerodon

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

Corollary 5.1.1.14. Let $q: X \rightarrow S$ and $f: K \rightarrow X$ be morphisms of simplicial sets, and let $q': X_{f/} \rightarrow S_{ (q \circ f)/ }$ be the morphism induced by $q$. Let $\overline{e}: \overline{x} \rightarrow \overline{y}$ be an edge of the simplicial set $X_{f/}$, and let $e: x \rightarrow y$ be its image in $X$. If $e$ is $q$-cartesian, then $\overline{e}$ is $q'$-cartesian.

Proof. Since $e$ is $q$-cartesian, the restriction map

$\theta : X_{/e} \rightarrow X_{/y} \times _{ S_{/q(y)} } S_{/q(e)}$

is a trivial Kan fibration (Proposition 5.1.1.13). We wish to show that the restriction map

$\overline{\theta }: (X_{f/} )_{ / \overline{e} } \rightarrow (X_{f/} )_{ / \overline{y} } \times _{ (S_{(q \circ f)/} )_{ / q'( \overline{y} )}} (S_{ (q \circ f)/} )_{ / q'( \overline{e} ) }.$

is also a trivial Kan fibration. Using Remark 4.3.5.15, we can identify $\overline{e}$ with a morphism of simplicial sets $\overline{f}: K \rightarrow X_{/e}$, and $\overline{\theta }$ with the induced map

$( X_{/e} )_{\overline{f} / } \rightarrow (X_{/y} \times _{ S_{/q(y)} } S_{/q(e)})_{ (\theta \circ \overline{f}) / }.$

The desired result now follows from Corollary 4.3.7.17. $\square$