Kerodon

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

Lemma 8.6.5.15. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories, let $\kappa $ be an uncountable cardinal such that each fiber of $U$ is locally $\kappa $-small. Let $\widetilde{e}$ be an edge of the simplicial set $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ corresponding to a pair $(e, \mathscr {F} )$, where $e: C \rightarrow D$ is an edge of $\operatorname{\mathcal{C}}$ and $\mathscr {F}: \Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ is a functor. The following conditions are equivalent:

$(1)$

The edge $\widetilde{e}$ is $\pi ^{\operatorname{corep}}$-cocartesian (where $\pi ^{\operatorname{corep}}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa }) \rightarrow \operatorname{\mathcal{C}}$ denotes the projection map).

$(2)$

There exists an object $X \in \operatorname{\mathcal{E}}_{C}$, a vertex $\eta \in \mathscr {F}(X)$ which exhibits $\mathscr {F}|_{ \operatorname{\mathcal{E}}_{C} }$ as corepresented by the object $X$, and a $U$-cocartesian morphism $\overline{e}: X \rightarrow Y$ such that $U( \overline{e} ) = e$ and the vertex $\mathscr {F}( \overline{e} )( \eta ) \in \mathscr {F}(Y)$ exhibits $\mathscr {F}|_{ \operatorname{\mathcal{E}}_{D} }$ as corepresented by the object $Y$.

$(3)$

For every object $X \in \operatorname{\mathcal{E}}_{C}$, every vertex $\eta \in \mathscr {F}(X)$ which exhibits $\mathscr {F}|_{\operatorname{\mathcal{E}}_{C}}$ as corepresented by the object $X$, and every $U$-cocartesian morphism $\overline{e}: X \rightarrow Y$ satisfying $U( \overline{e} ) = e$, the vertex $\mathscr {F}( \overline{e} )( \eta ) \in \mathscr {F}(Y)$ exhibits $\mathscr {F}|_{ \operatorname{\mathcal{E}}_{D} }$ as corepresented by the object $Y$.

Proof. By virtue of Remark 8.6.5.7, we are free to enlarge the cardinal $\kappa $; we may therefore assume without loss of generality that $\kappa $ is regular and that the $\infty $-category $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is essentially $\kappa $-small. In this case, Variant 8.6.5.11 shows that $(1)$ is equivalent to the following:

$(1')$

The functor $\mathscr {F}$ is left Kan extended from the full subcategory $\operatorname{\mathcal{E}}_{C} \subseteq \Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$.

The equivalences $(1') \Leftrightarrow (2) \Leftrightarrow (3)$ now follow from Lemma 8.6.5.14. $\square$