# Kerodon

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

Corollary 8.2.2.13. Let $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ be $\infty$-categories, and suppose we are given a pair of functors $F_{-}, F_{+}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. Then $F_{-}$ and $F_{+}$ are isomorphic (as objects of the $\infty$-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$) if and only if there exists a morphism of couplings

8.34
$$\begin{gathered}\label{equation:isomorphism-of-functors-twisted-arrow} \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [r]^-{ \widetilde{F} } \ar [d] & \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}}} \end{gathered}$$

having the property that the functor $\widetilde{F}$ carries isomorphisms of $\operatorname{\mathcal{C}}$ (regarded as objects of $\operatorname{Tw}(\operatorname{\mathcal{C}})$) to isomorphisms of $\operatorname{\mathcal{D}}$ (regarded as objects of $\operatorname{Tw}(\operatorname{\mathcal{D}})$).

Proof. Suppose first that there exists an isomorphism of functors $\alpha : F_{-} \rightarrow F_{+}$. Since the projection map $\operatorname{Tw}(\operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{D}}^{\operatorname{op}} \times \operatorname{\mathcal{D}}$ is an isofibration, we can use Corollary 4.4.5.6 to lift the natural transformation

$(\operatorname{id}\times \alpha ): F_{-}^{\operatorname{op}} \times F_{+} \rightarrow F_{-}^{\operatorname{op}} \times F_{-}$

to an isomorphism $\widetilde{F} \rightarrow \operatorname{Tw}(F_{-})$ in the $\infty$-category $\operatorname{Fun}( \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{Tw}(\operatorname{\mathcal{D}}) )$, so that we have a commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [r]^-{ \widetilde{F} } \ar [d] & \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}}}$

where $\widetilde{F}$ carries isomorphisms of $\operatorname{\mathcal{C}}$ to isomorphisms of $\operatorname{\mathcal{D}}$.

We now prove the converse. Suppose we are given a commutative diagram (8.34), where $\widetilde{F}$ carries isomorphisms of $\operatorname{\mathcal{C}}$ to isomorphisms of $\operatorname{\mathcal{D}}$. Applying Theorem 8.2.2.11, we deduce that the triple $( F_{-}, \widetilde{F}, F_{+} )$ is initial when viewed as an object of the $\infty$-category $\{ F_{-} \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})^{\operatorname{op}} } \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{Tw}(\operatorname{\mathcal{D}}) )$. Applying Example 8.2.2.12 (and Corollary 4.6.7.15), we deduce that $( F_{-}, \widetilde{F}, F_{+} )$ is isomorphic to $( F_{-}, \operatorname{Tw}(F_{-}), F_{-} )$ as an object of the $\infty$-category $\{ F_{-} \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})^{\operatorname{op}} } \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{Tw}(\operatorname{\mathcal{D}}) )$. In particular, $F_{+}$ is isomorphic to $F_{-}$ as an object of $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. $\square$