Kerodon

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

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

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

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

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

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

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

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$