# Kerodon

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

Proposition 5.1.4.17. Let $q: X \rightarrow S$ be a cartesian fibration of simplicial sets and let $f: K \rightarrow X$ be any morphism of simplicial sets. Then:

$(1)$

The induced map $q': X_{/f} \rightarrow S_{/(q \circ f)}$ is a cartesian fibration of simplicial sets.

$(2)$

An edge $e$ of $X_{/f}$ is $q'$-cartesian if and only if its image in $X$ is $q$-cartesian.

Proof. The morphism $q'$ factors as a composition

$X_{/f} \xrightarrow {u} X \times _{S} S_{/(q \circ f)} \xrightarrow {v} S_{ /(q \circ f)}.$

Since $q$ is an inner fibration, the morphism $u$ is a right fibration (Proposition 4.3.6.8). In particular, $u$ is a cartesian fibration and every edge of $X_{/f}$ is $u$-cartesian (Proposition 5.1.4.14). The morphism $v$ is a pullback of $q$, and is therefore a cartesian fibration (Remark 5.1.4.6). Moreover, an edge of $X \times _{S} S_{/(q \circ f)}$ is $v$-cartesian if and only if its image in $X$ is $q$-cartesian. Assertions $(1)$ and $(2)$ now follow from Proposition 5.1.4.13. $\square$