# Kerodon

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

Proposition 5.1.4.16. Let $q: X \rightarrow S$ be a cartesian fibration of simplicial sets, and let $X' \subseteq X$ be a full simplicial subset with the following property:

$(\ast )$

For every vertex $y \in X'$ and every edge $\overline{e}: \overline{x} \rightarrow q(y)$ in $S$, there exists a vertex $x \in X'$ and a $q$-cartesian edge $e: x \rightarrow y$ of $X$ satisfying $q(e) = \overline{e}$.

Then $q' = q|_{X'}$ is a cartesian fibration from $X'$ to $S$. Moreover, an edge $e$ of $X'$ is $q'$-cartesian if and only if it is $q$-cartesian.

Proof. Since the inclusion map $X' \hookrightarrow X$ is an inner fibration (see Definition 4.1.2.15), the restriction $q|_{X'}$ is also an inner fibration. Remark 5.1.1.7 guarantees that every edge of $X'$ which is $q$-cartesian is also $q'$-cartesian, so that $(\ast )$ immediately guarantees that $q'$ is a cartesian fibration. To complete the proof, we must show that if $e: x \rightarrow z$ is a $q'$-cartesian edge of $X'$, then $e$ is $q$-cartesian when viewed as an edge of $X$. Applying $(\ast )$, we can choose a $q$-cartesian edge $e': y \rightarrow z$ satisfying $q(e') = q(e)$, where $y$ belongs to $X'$. Then $e'$ is also $q'$-cartesian, so Remark 5.1.3.8 guarantees that there exists a $2$-simplex

$\xymatrix@R =50pt@C=50pt{ & y \ar [dr]^{e'} & \\ x \ar [ur]^{u} \ar [rr] & & z }$

of $X'$, where $u$ is an isomorphism in the $\infty$-category $\{ q(x) \} \times _{S} X'$. It follows that $u$ is also an isomorphism in the $\infty$-category $\{ q(x) \} \times _{S} X$, and is therefore $q$-cartesian (Proposition 5.1.4.11). Applying Proposition 5.1.4.12, we see that the edge $e$ is also $q$-cartesian. $\square$