# Kerodon

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

Proposition 5.3.6.6. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be a cocartesian fibration of simplicial sets and let $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a cartesian fibration of simplicial sets. Then postcomposition with $V$ induces a cartesian fibration of simplicial sets

$V': \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}).$

Moreover, an edge $e$ of $\operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ is $V'$-cocartesian if and only if it satisfies the following condition:

$(\ast )$

Write $e = (\overline{e}, f)$, where $\overline{e}$ is an edge of $\operatorname{\mathcal{B}}$ and $f: \Delta ^1 \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is a morphism of simplicial sets. Let $U_{\overline{e}}: \Delta ^1 \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \Delta ^1$ be given by projection onto the first factor. Then $f$ carries $U_{\overline{e}}$-cocartesian morphisms of $\Delta ^1 \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$ to $V$-cartesian morphisms of $\operatorname{\mathcal{D}}$.

Proof of Proposition 5.3.6.6. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be a cocartesian fibration of simplicial sets, let $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a cartesian fibration of simplicial sets, and let $V': \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}})$ be given by postcomposition with $V$. We first claim that $V'$ is an inner fibration. To prove this, we may assume without loss of generality that $\operatorname{\mathcal{B}}$ is a standard simplex, so that $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ is a cocartesian fibration of $\infty$-categories. Proposition 5.3.6.1 then guarantees that $U$ is exponentiable, so that $V'$ is an isofibration (Proposition 4.5.9.17) and therefore an inner fibration by virtue of Remark 4.5.5.7.

Let us say that an edge of $\operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ is special if it satisfies condition $(\ast )$ appearing in the statement of Proposition 5.3.6.6. Lemma 5.3.6.11 guarantees that every special edge of $\operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ is $V'$-cartesian. Moreover, if $Y$ is a vertex of $\operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ and $\overline{e}: \overline{X} \rightarrow V'(Y)$ is an edge of $\operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}})$, then Lemma 5.3.6.12 guarantees that there exists a special edge $e: X \rightarrow Y$ of $\operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ satisfying $V'(e) = \overline{e}$. It follows that $V'$ is a cartesian fibration of simplicial sets.

To complete the proof of Proposition 5.3.6.6, we must show that every $V'$-cartesian edge $e: X \rightarrow Y$ of $\operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ is special. Without loss of generality we may assume that $\operatorname{\mathcal{B}}= \Delta ^1$ and that $e$ lies over the nondegenerate edge of $\operatorname{\mathcal{B}}$, so that $e$ corresponds to a functor of $\infty$-categories $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. Replacing $\operatorname{\mathcal{D}}$ by the fiber product $\operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}$, we can assume that $\operatorname{\mathcal{E}}= \operatorname{\mathcal{C}}$ and that $V \circ F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ is the identity functor, so that $V$ is a cartesian fibration of $\infty$-categories. Using Lemma 5.3.6.12, we can choose a special edge $e': X' \rightarrow Y$ of $\operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}},\operatorname{\mathcal{D}})$ satisfying $V'(e') = V'(e)$, corresponding to another functor $F': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ satisfying $V \circ F' = \operatorname{id}_{\operatorname{\mathcal{C}}}$. Since $e'$ is also $V'$-cartesian, it is isomorphic to $e$ as an object of the $\infty$-category $\operatorname{Fun}_{ / \operatorname{\mathcal{B}}}( \Delta ^1, \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}},\operatorname{\mathcal{D}}) )$. It follows that $F$ and $F'$ are isomorphic as objects of the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. If $u$ is a $U$-cocartesian edge of $\operatorname{\mathcal{C}}$, then $F(u)$ is isomorphic to the $V$-cartesian morphism $E'(u)$ (as an object of the $\infty$-category $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{D}})$), and is therefore also $V$-cartesian (Corollary 5.1.2.5). $\square$