Kerodon

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

Proposition 8.6.4.8. Let $\kappa $ be an uncountable cardinal and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets which is locally $\kappa $-small (Variant 4.7.9.2). Then the evaluation map

\[ \operatorname{ev}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa }) \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa } \quad \quad ((C, \mathscr {F}_{C}), X) \mapsto \mathscr {F}_{C}(X) \]

exhibits the projection map $\pi ^{\operatorname{corep}}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{<\kappa }) \rightarrow \operatorname{\mathcal{C}}$ as a cocartesian dual of $U$ (in the sense of Variant 8.6.3.13).

Proof of Proposition 8.6.4.8. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, and let $\kappa $ be an uncountable cardinal such that each fiber of $U$ is locally $\kappa $-small. It follows from Proposition 8.6.4.12 that the projection map $\pi ^{\operatorname{corep}}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of simplicial sets. We wish to show that the evaluation map

\[ \operatorname{ev}: \operatorname{Fun}^{\operatorname{corep}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa } \quad \quad ( (C, \mathscr {F}_{C}), X) \mapsto \mathscr {F}_{C}(X) \]

satisfies conditions $(a)$ and $(b)$ of Definition 8.6.3.12. Condition $(a)$ asserts that, for each vertex $C \in \operatorname{\mathcal{C}}$, the evaluation map

\[ \operatorname{ev}_{C}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{S}}^{< \kappa } ) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{S}}^{< \kappa } \quad \quad (\mathscr {F},X) \mapsto \mathscr {F}(X) \]

is a balanced profunctor; this follows from Corollary 8.3.2.21. Assertion $(b)$ is a restatement of the implication $(1) \Rightarrow (3)$ of Lemma 8.6.4.15. $\square$