Kerodon

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

Corollary 8.2.4.4. Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ and $\mu : \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{+}$ be couplings of $\infty $-categories which are representable by functors $G: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$ and $H: \operatorname{\mathcal{D}}_{+} \rightarrow \operatorname{\mathcal{D}}_{-}$, respectively. Let $F_{-}: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{D}}_{-}$ and $F_{+}: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{D}}_{+}$ be functors. The following conditions are equivalent:

$(1)$

The functors $H \circ F_{+}$ and $F_{-} \circ G$ are isomorphic (as objects of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{-} )$. That is, the diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{+} \ar [r]^-{ F_{+} } \ar [d]^{ G } & \operatorname{\mathcal{D}}_{+} \ar [d]^{H} \\ \operatorname{\mathcal{C}}_{-} \ar [r]^-{ F_{-} } & \operatorname{\mathcal{D}}_{-} } \]

commutes up to isomorphism.

$(2)$

There is a morphism of couplings

8.43
\begin{equation} \begin{gathered}\label{equation:commutativity-as-morphism-of-coupling0} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{ \widetilde{F} } \ar [d]^{\lambda } & \operatorname{\mathcal{D}}\ar [d]^{\mu } \\ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}^{+} \ar [r]^-{ F_{-}^{\operatorname{op}} \times F_{+} } & \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{+}, } \end{gathered} \end{equation}

where the functor $\widetilde{F}$ carries universal objects of $\operatorname{\mathcal{C}}$ to universal objects of $\operatorname{\mathcal{D}}$.

Proof. Choose morphisms of couplings

8.44
\begin{equation} \begin{gathered}\label{equation:commutativity-as-morphism-of-coupling} \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}) \ar [r]^-{ \widetilde{G} } \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{\lambda } & \operatorname{\mathcal{D}}\ar [r]^-{ \widetilde{H} } \ar [d]^{\mu } & \operatorname{Tw}( \operatorname{\mathcal{D}}_{-} ) \ar [d] \\ \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}}_{+} & \operatorname{\mathcal{D}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{D}}_{+} \ar [r]^-{ \operatorname{id}\times H } & \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{-}, } \end{gathered} \end{equation}

which exhibit $\lambda $ and $\mu $ as represented by $G$ and $H$, respectively. We first prove that $(2)$ implies $(1)$. Suppose there exists a diagram (8.43), where $\widetilde{F}$ carries universal objects of $\operatorname{\mathcal{C}}$ to universal objects of $\operatorname{\mathcal{D}}$. Composing with the morphisms (8.44), we obtain a morphism of twisted arrow couplings

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

where the functor $\widetilde{H} \circ \widetilde{F} \circ \widetilde{G}$ carries isomorphisms in $\operatorname{\mathcal{C}}_{+}$ to isomorphisms in $\operatorname{\mathcal{D}}_{-}$. Applying Corollary 8.2.2.13, we deduce that the functors $F_{-} \circ G$ and $H \circ F_{+}$ are isomorphic.

We now show that $(1)$ implies $(2)$. Since $\lambda $ is representable and the twisted arrow pairing $\operatorname{Tw}(\operatorname{\mathcal{D}}_{-}) \rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{-}$ is corepresentable, Theorem 8.2.2.11 guarantees that there exists a morphism of pairings

8.45
\begin{equation} \begin{gathered}\label{equation:commutativity-as-morphism-of-coupling2} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [d]^{\lambda } \ar [r]^-{ \widetilde{T} } & \operatorname{Tw}(\operatorname{\mathcal{D}}_{-} ) \ar [d] \\ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+} \ar [r]^-{ F^{\operatorname{op}}_{-} \times T_{+} } & \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{-}, } \end{gathered} \end{equation}

where $\widetilde{T}$ carries universal objects of $\operatorname{\mathcal{C}}$ to isomorphisms in the $\infty $-category $\operatorname{\mathcal{D}}_{-}$. Composing with the pairing on the left half of (8.44), we obtain a morphism of twisted arrow pairings

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

Applying Corollary 8.2.2.13, we conclude that $T_{+}$ is isomorphic to the functor $F_{-} \circ G$. If condition $(1)$ is satisfied, then $T_{+}$ is also isomorphic to the functor $H \circ F_{+}$. Replacing (8.45) by an isomorphic objects of $\infty $-category $\{ F_{-} \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{D}}_{-})^{\operatorname{op}}} \times \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{D}}_{-} ) )$, we may assume without loss of generality that $T_{+}$ is equal to $H \circ F_{+}$. Invoking the universal property of Proposition 8.2.3.9, we can further assume that (8.45) factors as a composition

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

Since $\widetilde{T} = \widetilde{H} \circ \widetilde{F}$ carries universal objects of $\operatorname{\mathcal{D}}$ to isomorphisms in $\operatorname{\mathcal{D}}_{-}$, the functor $\widetilde{F}$ carries universal objects of $\operatorname{\mathcal{C}}$ to universal objects of $\operatorname{\mathcal{D}}$. $\square$