# Kerodon

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

Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$ be a coupling of $\infty$-categories which is both representable and corepresentable. Using Theorem 8.2.3.4 (and its dual), we can choose a functor $G: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$ which represents $\lambda$ and a functor $F: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{C}}_{+}$ which corepresents $\lambda$. Either of these functors determines the pairing $\lambda$ up to equivalence, and therefore determines the other up to isomorphism. Our goal in this section is to establish the following more precise result:

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$.

We first establish a weaker version of Theorem 8.2.5.1.

Proposition 8.2.5.2. Let $\lambda = (\lambda _{-}, \lambda _{+}): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$ be coupling of $\infty$-categories which is representable by a functor $G: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$. The following conditions are equivalent:

$(1)$

The coupling $\lambda$ is corepresentable.

$(2)$

The functor $G$ admits a left adjoint.

Proof. By virtue of the criterion of Corollary 6.2.4.2, it will suffice to show that for each object $X \in \operatorname{\mathcal{C}}_{-}$, the following conditions are equivalent:

$(1_ X)$

There exists a couniversal object $\widetilde{X} \in \operatorname{\mathcal{C}}$ satisfying $\lambda _{-}( \widetilde{X} ) = X$.

$(2_ X)$

The $\infty$-category $( \operatorname{\mathcal{C}}_{-} )_{X/} \times _{ \operatorname{\mathcal{C}}_{-} } \operatorname{\mathcal{C}}_{+}$ has an initial object.

Note that Proposition 8.1.2.5 supplies an equivalence $(\operatorname{\mathcal{C}}_{-})_{X/} \hookrightarrow \{ X\} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{Tw}( \operatorname{\mathcal{C}}_{-} )$ of $\infty$-categories which are left-fibered over $\operatorname{\mathcal{C}}_{-}$. Restricting along the functor $G$, we obtain an equivalence of $\infty$-categories

$( \operatorname{\mathcal{C}}_{-} )_{X/} \times _{ \operatorname{\mathcal{C}}_{-} } \operatorname{\mathcal{C}}_{+} \hookrightarrow \{ X\} \times _{ \operatorname{\mathcal{C}}_{-} }^{\operatorname{op}} \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) \times _{ \operatorname{\mathcal{C}}_{-} } \operatorname{\mathcal{C}}_{+}.$

Since $\lambda$ is representable by $G$, there exists a categorical pullback square

$\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}}_{-} }$

which induces an equivalence of $\infty$-categories

$\{ X\} \times _{\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}} \operatorname{\mathcal{C}}\rightarrow \{ X\} \times _{ \operatorname{\mathcal{C}}_{-} }^{\operatorname{op}} \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) \times _{ \operatorname{\mathcal{C}}_{-} } \operatorname{\mathcal{C}}_{+}.$

The equivalence of $(1_ X)$ and $(2_ X)$ now follows from Corollary 4.6.6.22. $\square$

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.36
$$\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.37
$$\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.10, 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.36) 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.37) is a couniversal object of $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}), \operatorname{\mathcal{C}})$ (Theorem 8.2.2.9). $\square$