Kerodon

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

Corollary 8.6.5.19. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, $U^{\vee }: \operatorname{\mathcal{E}}^{\vee } \rightarrow \operatorname{\mathcal{C}}$, and $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets, let $\kappa $ be an uncountable cardinal, and let $\mathscr {K}: \operatorname{\mathcal{E}}^{\vee } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ exhibit $U^{\vee }$ as a cocartesian dual of $U$. Then:

$(1)$

Composition with $\mathscr {K}$ induces a fully faithful functor

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}^{\vee } ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{D}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}^{\vee }, \operatorname{\mathcal{S}}^{ < \kappa } ). \]

The essential image is spanned by the weak $\operatorname{\mathcal{C}}$-families of corepresentable profunctors.

$(2)$

A morphism $F \in \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}^{\vee } )$ carries $V$-cocartesian edges of $\operatorname{\mathcal{D}}$ to $U^{\vee }$-cocartesian edges of $\operatorname{\mathcal{E}}^{\vee }$ if and only if the composite map

\[ \operatorname{\mathcal{D}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\xrightarrow {F \times \operatorname{id}} \operatorname{\mathcal{E}}^{\vee } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\xrightarrow { \mathscr {K} } \operatorname{\mathcal{S}}^{<\kappa } \]

is a $\operatorname{\mathcal{C}}$-family of corepresentable profunctors.

$(3)$

A morphism $F \in \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}^{\vee } )$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$ if and only if the composite map

\[ \operatorname{\mathcal{D}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\xrightarrow {F \times \operatorname{id}} \operatorname{\mathcal{E}}^{\vee } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\xrightarrow { \mathscr {K} } \operatorname{\mathcal{S}}^{<\kappa } \]

exhibits $V$ as a cocartesian dual of $U$

Proof. We can identify $\mathscr {K}$ with a morphism $G \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}^{\vee }, \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) )$. It follows from Proposition 8.6.5.18 that $G$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$. We can therefore replace $\operatorname{\mathcal{E}}^{\vee }$ by $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ and $\mathscr {K}$ by 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 }$. In this case, assertions $(1)$, $(2)$, and $(3)$ follow immediately from the corresponding assertions of Proposition 8.6.5.18. $\square$