# Kerodon

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

Proposition 5.3.7.9. Let $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of simplicial sets, let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. Then:

$(1)$

The projection map $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of simplicial sets.

$(2)$

Let $e: X \rightarrow Y$ be a $\pi$-cocartesian edge of the simplicial set $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. If $X$ belongs to the simplicial subset $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$, then $Y$ also belongs to the simplicial subset $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$.

$(3)$

The morphism $\pi$ restricts to a cocartesian fibration $\pi ^{\operatorname{CCart}}: \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$.

$(4)$

An edge of the simplicial set $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$ is $\pi ^{\operatorname{CCart}}$-cocartesian if and only if it is $\pi$-cocartesian.

Proof. Assertion $(1)$ follows from Proposition 5.3.6.6 (after passing to opposite simplicial sets). To prove $(2)$, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^1$ and $\pi (e)$ is the nondegenerate edge of $\operatorname{\mathcal{C}}$. In this case, the simplicial sets $\operatorname{\mathcal{D}}$ and $\operatorname{\mathcal{E}}$ are $\infty$-categories, and we can identify the edge $e$ with a morphism of simplicial sets $E: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ satisfying $V \circ E = \operatorname{id}_{\operatorname{\mathcal{D}}}$. Let $u: D \rightarrow D'$ be a morphism in the $\infty$-category $\operatorname{\mathcal{D}}_1 = \{ 1\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$; we wish to show that $E(u)$ is a $V$-cocartesian morphism of $\operatorname{\mathcal{E}}$. To prove this, let $G: \operatorname{\mathcal{D}}_{1} \rightarrow \operatorname{\mathcal{D}}_0 = \{ 0\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ be given by contravariant transport along the nondegenerate edge of $\operatorname{\mathcal{C}}$, so that we have a commutative diagram

$\xymatrix@R =50pt@C=50pt{ G(D) \ar [d]^{ G(u) } \ar [r] & D \ar [d]^{u} \\ G(D') \ar [r] & D', }$

in the $\infty$-category where the horizontal maps are $U$-cartesian. Our assumption that $e$ is $\pi$-cocartesian guarantees that the functor $E$ carries $U$-cartesian morphisms of $\operatorname{\mathcal{D}}$ to $V$-cocartesian morphisms of $\operatorname{\mathcal{E}}$ (Proposition 5.3.6.6). We therefore obtain a commutative diagram

$\xymatrix@R =50pt@C=50pt{ (E \circ G)(D) \ar [d]^{ (E \circ G)(u) } \ar [r] & E(D) \ar [d]^{ E(u) } \\ (E \circ G)(D') \ar [r] & E(D' ), }$

where the horizontal maps are $V$-cocartesian. By virtue of Corollary 5.1.2.4, it will suffice to show that the morphism $(E \circ G)(u)$ is $V$-cocartesian, which follows from our assumption that $X$ belongs to $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$. This completes the proof of $(2)$; assertions $(3)$ and $(4)$ then follow by applying Proposition 5.1.4.16. $\square$