Kerodon

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

Lemma 9.4.8.7. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a flat inner fibration of $\infty $-categories, let $\kappa $ be an uncountable regular cardinal for which $U$ is essentially $\kappa $-small, and let

\[ H: \operatorname{\mathcal{E}}^{\operatorname{op}} \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa } \]

be a relative $\operatorname{Hom}$-functor for $U$. Then the induced map $h: \operatorname{\mathcal{E}}^{\operatorname{op}} \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger }$ exhibits $\operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}^{\operatorname{op}}$ (relative to $\operatorname{\mathcal{C}}^{\operatorname{op}}$).

Proof. Let us identify $H$ with a functor $F: \operatorname{\mathcal{E}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$. If $X$ an object of $\operatorname{\mathcal{E}}$ having image $C = U(X)$ and $u: C \rightarrow D$ is a morphism of $\operatorname{\mathcal{C}}$, our assumption that $U$ is a cocartesian fibration guarantees that we can lift $u$ to a $U$-cocartesian morphism $\widetilde{u}: X \rightarrow Y$ of $\operatorname{\mathcal{E}}$. In this case, we can identify $F(X,u)$ with a functor $\operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ which is corepresented by the object $Y$. It follows that $F$ factors through the full subcategory $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \subseteq \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ of Construction 8.6.5.6. Unwinding the definitions, we have a commutative diagram

9.48
\begin{equation} \begin{gathered}\label{equation:relative-Yoneda-determines} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [r]^-{F} \ar [d]^{h \times \operatorname{id}} & \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \ar [d] \\ \operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [r]^-{\operatorname{ev}} & \operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ). } \end{gathered} \end{equation}

Let $V: \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \rightarrow \operatorname{\mathcal{C}}$ and $V^{\dagger }: \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ denote the projection maps, and set $V^{\operatorname{corep}} = V|_{ \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) }$. Then the lower horizontal map exhibits $V^{\dagger }$ as a cartesian conjugate of $V$ (Proposition 8.6.2.3), and the upper horizontal map exhibits $U^{\operatorname{op}}$ as a cartesian conjugate of $V^{\operatorname{corep}}$ (Theorem 8.6.6.15). Moreover, the inclusion map $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \subseteq \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ exhibits $\operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ as a fiberwise $\kappa $-cocompletion of $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ (Example 9.4.2.5). Applying Proposition 9.4.3.3, we conclude that $h$ exhibits $\operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger }$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}^{\operatorname{op}}$. $\square$