Kerodon

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

Variant 8.6.4.11. Let $\kappa $ be an uncountable regular cardinal, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an exponentiable inner fibration which is essentially $\kappa $-small, and let $\operatorname{\mathcal{D}}$ be an $\infty $-category which is $\kappa $-cocomplete. Then the projection map $\pi : \operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration. Moreover, an edge $\widetilde{e}$ of $\operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}},\operatorname{\mathcal{D}})$ is $\pi $-cocartesian if and only if satisfies the following condition:

$(\ast )$

Write $\widetilde{e} = (e, F_ e)$, where $e$ is an edge of $\operatorname{\mathcal{C}}$ and $F_{e}: \Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ is a functor of $\infty $-categories. Then $F_{e}$ is left Kan extended from the full subcategory $\{ 0\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$.

Proof. Corollary 4.5.9.18 guarantees that $\pi $ is an isofibration, and Corollary 7.3.7.9 guarantees that every edge of $\operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}},\operatorname{\mathcal{D}})$ which satisfies condition $(\ast )$ is $\pi $-cocartesian. Suppose we are given a vertex $\widetilde{C} = (C, F_ C)$ of $\operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$, where $C$ is a vertex of $\operatorname{\mathcal{C}}$ and $F_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{D}}$ is a functor of $\infty $-categories. If $e: C \rightarrow C'$ is an edge of $\operatorname{\mathcal{C}}$, then Proposition 7.6.7.13 guarantees that $F_{C}$ admits a left Kan extension $F_{e}: \Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$, which we can identify with an edge $\widetilde{e}$ of $\operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ satisfying $\pi ( \widetilde{e} ) = e$. By construction, the morphism $\widetilde{e}$ satisfies condition $(\ast )$, and is therefore $\pi $-cocartesian by virtue of Corollary 7.3.7.9. Allowing $\widetilde{C}$ and $e$ to vary, we conclude that $\pi $ is a cocartesian fibration. To complete the proof, it will suffice to show that every $\pi $-cocartesian edge $\widetilde{e}'$ of $\operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ satisfies condition $(\ast )$. Let us identify $\widetilde{e}'$ with a pair $(e, F'_{e})$, where $e$ is an edge of $\operatorname{\mathcal{B}}$ and $F'_{e}: \Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ is a functor. Using the preceding argument, we see that the restriction $F'_{e}|_{ \{ 0\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}}$ admits a left Kan extension $F_{e}: \Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$, corresponding to another edge $\widetilde{e}$ of $\operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}},\operatorname{\mathcal{D}})$. By construction, $\widetilde{e}$ satisfies condition $(\ast )$ and is therefore $\pi $-cocartesian. Invoking the uniqueness of cocartesian lifts (Remark 5.1.3.8), we deduce that the functors $F_{e}$ and $F'_{e}$ are isomorphic. It follows that $F'_{e}$ is also left Kan extended from $\{ 0\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ (Remark 7.3.3.17), so that $\widetilde{e}'$ satisfies condition $(\ast )$ as desired. $\square$