Kerodon

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

Theorem 8.2.3.4. Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ be a coupling of $\infty $-categories. Then $\lambda $ is representable (in the sense of Definition 8.2.1.3) if and only there exists a functor $G: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$ such that $\lambda $ is representable by $G$ (in the sense of Definition 8.2.3.1). If this condition is satisfied, then the functor $G$ is uniquely determined up to isomorphism.

Proof of Theorem 8.2.3.4. Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ be a coupling of $\infty $-categories. It follows from Proposition 8.2.3.7 that $\lambda $ is representable by a functor $G: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$ if and only if it is representable and $G$ can be lifted to an initial object of the $\infty $-category $\operatorname{\mathcal{E}}= \{ \operatorname{id}\} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{C}}_{-} )^{\operatorname{op}} } \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{C}}_{-} ) )$. This immediately shows that $G$ is uniquely determined up to isomorphism. To prove existence, it suffices to show that if $\lambda $ is representable then $\operatorname{\mathcal{E}}$ has an initial object. This follows from Theorem 8.2.2.11. $\square$