Kerodon

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

Proposition 8.2.4.3. Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ be a coupling of $\infty $-categories and let $G: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$ be a functor. The following conditions are equivalent:

$(1)$

The coupling $\lambda $ is representable by $G$ (in the sense of Definition 8.2.3.1).

$(2)$

There exists a morphism of couplings

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}( \operatorname{\mathcal{C}}_{+} ) \ar [r]^-{ \widetilde{G} } \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{ \lambda } \\ \operatorname{\mathcal{C}}^{\operatorname{op}}_{+} \times \operatorname{\mathcal{C}}_{+} \ar [r]^-{ G^{\operatorname{op}} \times \operatorname{id}} & \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+} } \]

which exhibits $\lambda $ as represented by $G$ (in the sense of Definition 8.2.4.1).

Proof. We first show that $(2)$ implies $(1)$. Suppose that there exists a morphism of couplings

8.41
\begin{equation} \begin{gathered}\label{equation:duality-functor-left-to-right-fix} \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}( \operatorname{\mathcal{C}}_{+} ) \ar [r]^-{ \widetilde{G} } \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{ \lambda } \\ \operatorname{\mathcal{C}}^{\operatorname{op}}_{+} \times \operatorname{\mathcal{C}}_{+} \ar [r]^-{ G^{\operatorname{op}} \times \operatorname{id}} & \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+} } \end{gathered} \end{equation}

which exhibits $\lambda $ as represented by $G$ (in the sense of Definition 8.2.4.1). For each object $C_{+} \in \operatorname{\mathcal{C}}_{+}$, the functor $\widetilde{G}$ carries $\operatorname{id}_{C}$ to a universal object of $C \in \operatorname{\mathcal{C}}$ satisfying $\lambda _{+}(C) = C_{+}$. It follows that the coupling $\lambda $ is representable. Theorem 8.2.3.4, guarantees that there exists a functor $G': \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$ such that $\lambda $ is representable by $G'$. Choose morphism of couplings

8.42
\begin{equation} \begin{gathered}\label{equation:duality-functor-left-to-right2-fix} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{ \widetilde{G}' } \ar [d]^{\lambda } & \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) \ar [d] \\ \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+} \ar [r]^-{ \operatorname{id}\times G' } & \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{-}, } \end{gathered} \end{equation}

which exhibits $\lambda $ as represented by $G'$ (in the sense of Definition 8.2.3.5). Composing (8.42) with (8.41), we obtain a morphism of twisted arrow couplings

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}(\operatorname{\mathcal{C}}_{+} ) \ar [r]^-{ \widetilde{G}' \circ \widetilde{G} } \ar [d] & \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) \ar [d] \\ \operatorname{\mathcal{C}}_{+}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+} \ar [r]^-{ G^{\operatorname{op}} \times G'} & \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+} } \]

where the functor $\widetilde{G}' \circ \widetilde{G}$ carries isomorphisms of $\operatorname{\mathcal{C}}_{+}$ to isomorphisms of $\operatorname{\mathcal{C}}_{-}$. Invoking Corollary 8.2.2.13, we deduce that the functors $G$ and $G'$ are isomorphic, so that $\lambda $ is also representable by $G$ (Remark 8.2.3.2).

We now show that $(1)$ implies $(2)$. Assume that $\lambda $ is representable by $G$. Setting $G' = G$, we can choose a diagram (8.42) which exhibits $\lambda $ as represented by $G$. Applying Proposition 8.2.3.9, we deduce that composition with $\widetilde{G}'$ induces a homotopy equivalence of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ \{ G\} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{-} )^{\operatorname{op}} } \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+} ), \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{+} ) } \{ \operatorname{id}\} \ar [d]^{\theta } \\ \{ G\} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{-} )^{\operatorname{op}} } \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+} ), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) ) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{-} ) } \{ G \} . } \]

In particular, there exists an object $(G, \widetilde{G}, \operatorname{id}) \in \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+} ), \operatorname{\mathcal{C}})$ such that $(\operatorname{id}, \widetilde{G}', G) \circ (G, \widetilde{G}, \operatorname{id})$ is isomorphic to $(G, \operatorname{Tw}(G), G)$ in the $\infty $-category $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-} ) )$. In particular, the functor $\widetilde{G}' \circ \widetilde{G}: \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}) \rightarrow \operatorname{Tw}(\operatorname{\mathcal{C}}_{-})$ is isomorphic to the functor $\operatorname{Tw}(G)$, and therefore carries isomorphisms of $\operatorname{\mathcal{C}}_{+}$ to isomorphisms of $\operatorname{\mathcal{C}}_{-}$. It follows that the functor $\widetilde{G}: \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}) \rightarrow \operatorname{\mathcal{C}}$ carries isomorphisms in $\operatorname{\mathcal{C}}_{+}$ to universal objects of $\operatorname{\mathcal{C}}$, so that the diagram (8.41) exhibits $\lambda $ as represented by $G$. $\square$