# Kerodon

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

Theorem 8.2.5.1. Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$ be a coupling of $\infty$-categories which is representable by a functor $G: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$. Then a functor $F: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{C}}_{+}$ corepresents the coupling $\lambda$ if and only if it is left adjoint to $G$.

Proof of Theorem 8.2.5.1. Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$ be a coupling of $\infty$-categories which is representable by a functor $G: \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \rightarrow \operatorname{\mathcal{C}}_{+}$. By virtue of Proposition 8.2.5.2, the functor $G$ admits a left adjoint if and only if the coupling $\lambda$ is corepresentable. If this condition is satisfied, then there exists a functor $F: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{C}}_{+}$ which corepresents the coupling $\lambda$; moreover, $F$ is uniquely determined up to isomorphism (Theorem 8.2.0.4). We will complete the proof by showing that $F$ is a left adjoint of $G$.

Choose a diagram

8.50
$$\begin{gathered}\label{equation:adjunction-and-duality0} \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}$$

which exhibits $\lambda$ as represented by $G$ (see Definition 8.2.3.5). Then, for each universal object $C \in \operatorname{\mathcal{C}}$, the image $\widetilde{G}(C) \in \operatorname{Tw}( \operatorname{\mathcal{C}}_{-} )$ corresponds to an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}_{-}$ (Proposition 8.2.3.7). Using Proposition 8.2.4.3, we can choose a commutative diagram

8.51
$$\begin{gathered}\label{equation:adjunction-and-duality} \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}( \operatorname{\mathcal{C}}_{-} ) \ar [r]^-{ \widetilde{F} } \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{ \lambda } \\ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{-} \ar [r]^-{ \operatorname{id}\times F} & \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+} } \end{gathered}$$

which exhibits $\lambda$ as corepresented by $F$ (see Variant 8.2.4.5). It follows that the composite functor $\widetilde{F} \circ \widetilde{G}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ carries universal objects of $\operatorname{\mathcal{C}}$ to couniversal objects of $\operatorname{\mathcal{C}}$. Applying Theorem 8.2.4.6, we deduce that the diagram

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

is couniversal when viewed as an object of the $\infty$-category $\operatorname{Fun}_{\pm }(\operatorname{\mathcal{C}}, \operatorname{\mathcal{C}})$.

In particular, there exists an (essentially unique) morphism

$\widetilde{\epsilon }: (\operatorname{id}_{\operatorname{\mathcal{C}}_{-}}, \widetilde{F} \circ \widetilde{G}, F \circ G) \rightarrow ( \operatorname{id}_{\operatorname{\mathcal{C}}_{-}}, \operatorname{id}_{ \operatorname{\mathcal{C}}}, \operatorname{id}_{ \operatorname{\mathcal{C}}_{+} } )$

in the $\infty$-category $\{ \operatorname{id}_{ \operatorname{\mathcal{C}}_{-}} \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{C}}_{-} )^{\operatorname{op}} } \operatorname{Fun}_{\pm }(\operatorname{\mathcal{C}}, \operatorname{\mathcal{C}})$. Let $\epsilon : F \circ G \rightarrow \operatorname{id}_{ \operatorname{\mathcal{C}}_{+} }$ denote the image of $\widetilde{\epsilon }$ under the forgetful functor $\operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{+} )$. We will show that $\epsilon$ is the counit of an adjunction between $F$ and $G$.

Using Example 8.2.2.12, we see that the diagram

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

is couniversal when viewed as an object of the $\infty$-category $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-} ) )$. In particular, there exists an (essentially unique) morphism

$\widetilde{\eta }: ( \operatorname{id}_{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} }, \operatorname{id}_{ \operatorname{Tw}(\operatorname{\mathcal{C}}_{-})}, \operatorname{id}_{ \operatorname{\mathcal{C}}_{-} } ) \rightarrow ( \operatorname{id}_{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} }, \widetilde{G} \circ \widetilde{F}, G \circ F )$

in the $\infty$-category $\{ \operatorname{id}_{ \operatorname{\mathcal{C}}_{-} } \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{C}}_{-} )^{\operatorname{op}} } \operatorname{Fun}_{\pm }(\operatorname{Tw}(\operatorname{\mathcal{C}}_{-}), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}))$. Let $\eta : \operatorname{id}_{ \operatorname{\mathcal{C}}_{+} } \rightarrow G \circ F$ denote the image of $\widetilde{\eta }$ under the forgetful functor $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{C}}_{-} )$. We will complete the proof by showing that $\eta$ is compatible with $\epsilon$ up to homotopy, in the sense of Definition 6.2.1.1. For this, we must verify the following:

$(Z1)$

The identity isomorphism $\operatorname{id}_{ F}$ is a composition of the natural transformations

$F = F \circ \operatorname{id}_{ \operatorname{\mathcal{C}}_{-} } \xrightarrow {\operatorname{id}\circ \eta } F \circ G \circ F \xrightarrow { \epsilon \circ \operatorname{id}} \operatorname{id}_{ \operatorname{\mathcal{C}}_{+} } \times F = F$

in the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{C}}_{+} )$.

$(Z2)$

The identity isomorphism $\operatorname{id}_{ G }$ is a composition of the natural transformations

$G = \operatorname{id}_{ \operatorname{\mathcal{C}}_{-}} \circ G \xrightarrow {\eta \circ \operatorname{id}} G \circ F \circ G \xrightarrow { \operatorname{id}\circ \epsilon } G \times \operatorname{id}_{\operatorname{\mathcal{C}}_{+}} = G$

in the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{-} )$.

Using Theorem 8.2.4.6, we deduce that the diagram (8.50) is a couniversal object of $\operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{C}}_{-} )$: that is, it is initial when viewed as an object of the $\infty$-category $\operatorname{\mathcal{E}}= \{ \operatorname{id}_{ \operatorname{\mathcal{C}}_{-} } \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{C}}_{-} )^{\operatorname{op}}} \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) )$. It follows that the diagram

$\xymatrix@R =50pt@C=50pt{ & ( \operatorname{id}_{\operatorname{\mathcal{C}}_{-}}, \widetilde{G} \circ \widetilde{F} \circ \widetilde{G}, G \circ F \circ G) \ar [dr]^-{ \operatorname{id}\circ \widetilde{\epsilon }} & \\ ( \operatorname{id}_{\operatorname{\mathcal{C}}_{-}}, \widetilde{G}, G) \ar [ur]^{\widetilde{\eta } \circ \operatorname{id}} \ar [rr]^{ \operatorname{id}} & & ( \operatorname{id}_{\operatorname{\mathcal{C}}_{-}}, \widetilde{G}, G) }$

commutes up to homotopy in $\operatorname{\mathcal{E}}$. Assertion $(Z2)$ follows by applying the forgetful functor $\operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{C}}_{-})) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{-} )$. Assertion $(Z1)$ follows by a similar argument, using the observation that the diagram (8.51) is a couniversal object of $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}), \operatorname{\mathcal{C}})$ (Theorem 8.2.2.11). $\square$