Kerodon

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

Proposition 8.6.5.12. Let $\kappa $ be an uncountable regular cardinal and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets which is essentially $\kappa $-small. Then:

$(1)$

The projection map $\pi : \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \rightarrow \operatorname{\mathcal{C}}$ is both a cartesian fibration and a cocartesian fibration.

$(2)$

Let $\widetilde{e}$ be a $\pi $-cocartesian edge of the simplicial set $\operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{<\kappa } )$. If the source of $\widetilde{e}$ belongs to the simplicial subset $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$, then the target of $\widetilde{e}$ also belongs to the simplicial subset $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa })$.

$(3)$

The morphism $\pi $ restricts to a cocartesian fibration $\pi ^{\operatorname{corep}}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa }) \rightarrow \operatorname{\mathcal{C}}$. Moreover, an edge of $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ is $\pi ^{\operatorname{corep}}$-cocartesian if and only if it is $\pi $-cocartesian.

Proof. Assertion $(1)$ follows from Corollary 5.3.6.8 and Proposition 8.6.5.9 (since the $\infty $-category $\operatorname{\mathcal{S}}^{< \kappa }$ admits $\kappa $-small colimits; see Corollary 7.4.3.8). We will prove $(2)$. Let $\widetilde{e}: (C,\mathscr {F}_ C) \rightarrow (C', \mathscr {F}_{C'})$ be an edge of the simplicial set $\operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa })$ having image $e: C \rightarrow C'$ in $\operatorname{\mathcal{C}}$. Let $e_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C'}$ be given by covariant transport along $e$ for the cocartesian fibration $U$. If $\widetilde{e}$ is $\pi $-cocartesian, then we can identify $\mathscr {F}_{C'}$ with a left Kan extension of $\mathscr {F}_{C}$ along the functor $e_{!}$ (Remark 8.6.5.10). In particular, if the functor $\mathscr {F}_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{S}}$ is corepresentable by an object $X \in \operatorname{\mathcal{E}}_{C}$, then $\mathscr {F}_{C'}$ is corepresentable by the image $e_{!}(X) \in \operatorname{\mathcal{C}}_{C'}$ (Corollary 8.3.1.9). This proves assertion $(2)$, and assertion $(3)$ is a formal consequence (see Proposition 5.1.4.17). $\square$