# Kerodon

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

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 Remark 7.4.5.7). 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.16). $\square$