Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\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.17, 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.14). 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$