$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 5.1.5.13. Let $q: X \rightarrow S$ be a locally 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 locally cartesian fibration of simplicial sets.
- $(2)$
An edge $e$ of $X_{/f}$ is locally $q'$-cartesian if and only if its image in $X$ is locally $q$-cartesian.
Proof.
As in the proof of Proposition 5.1.4.18, we factor $q'$ as a composition
\[ X_{/f} \xrightarrow {u} X \times _{S} S_{/(q \circ f)} \xrightarrow {v} S_{ /(q \circ f)}, \]
where $u$ is a cartesian fibration and every edge of $X_{/f}$ is $u$-cartesian (Proposition 5.1.4.15). The morphism $v$ is a pullback of $q$, and is therefore a locally cartesian fibration (Remark 5.1.5.5). Moreover, an edge of $X \times _{S} S_{/(q \circ f)}$ is locally $v$-cartesian if and only if its image in $X$ is locally $q$-cartesian (Remark 5.1.3.5). Assertions $(1)$ and $(2)$ now follow from Remark 5.1.5.7.
$\square$