# Kerodon

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

Proposition 5.1.4.7. Let $q: X \rightarrow S$ be a morphism of simplicial sets. Then $q$ is a cartesian fibration if and only if, for every simplex $\sigma : \Delta ^ n \rightarrow S$, the projection map $q_{\sigma }: \Delta ^ n \times _{S} X \rightarrow \Delta ^ n$ is a cartesian fibration.

Proof. If $q$ is a cartesian fibration, then Remark 5.1.4.6 guarantees that every pullback of $q$ is a cartesian fibration. Conversely, suppose that for every $n$-simplex $\sigma : \Delta ^ n \rightarrow S$, the projection map $q_{\sigma }: \Delta ^ n \times _{S} X \rightarrow \Delta ^ n$ is a cartesian fibration. Applying this assumption in the case $n=1$, we conclude that for every vertex $y \in X$ and every edge $\overline{e}: \overline{x} \rightarrow q(y)$ of $S$, there exists a locally $q$-cartesian edge $e: x \rightarrow y$ satisfying $q(e) = \overline{e}$. Moreover, Remark 4.1.1.13 guarantees that $q$ is an inner fibration. It will therefore suffice to show that every locally $q$-cartesian edge $e$ of $X$ is $q$-cartesian. By virtue of Remark 5.1.1.12, it suffices to verify the analogous assertion for each of the projection maps $q_{\sigma }: \Delta ^ n \times _{S} X \rightarrow \Delta ^ n$, which follows from Remark 5.1.4.5 (since $q_{\sigma }$ is assumed to be a cartesian fibration). $\square$