Proposition 8.2.3.9. Let $\mu = (\mu _{-}, \mu _{+}): \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{+}$ be a coupling of $\infty $-categories, let $G: \operatorname{\mathcal{D}}_{+} \rightarrow \operatorname{\mathcal{D}}_{-}$ be a functor, and suppose we are given a morphism of couplings
8.39
\begin{equation} \begin{gathered}\label{equation:exhibits-as-representable-version1} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{D}}\ar [r]^-{ \widetilde{G} } \ar [d] & \operatorname{Tw}( \operatorname{\mathcal{D}}_{-} ) \ar [d] \\ \operatorname{\mathcal{D}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{D}}_{+} \ar [r]^-{ \operatorname{id}\times G } & \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{-}. } \end{gathered} \end{equation}
The following conditions are equivalent:
- $(1)$
The diagram (8.39) exhibits $\mu $ as represented by $G$ (in the sense of Definition 8.2.3.5).
- $(2)$
For every coupling of $\infty $-categories $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ and every pair of functors $F_{-}: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{D}}_{-}$ and $F_{+}: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{D}}_{+}$, composition with $\widetilde{G}$ induces a homotopy equivalence of Kan complexes
\[ \xymatrix@R =50pt@C=50pt{ \{ F_{-} \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{D}}_{-} )^{\operatorname{op}} } \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+}) } \{ F_{+} \} \ar [d] \\ \{ F_{-} \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{D}}_{-} )^{\operatorname{op}} } \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{D}}_{-} )) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{-}) } \{ G \circ F_{+} \} } \]
- $(3)$
For every coupling of $\infty $-categories $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ and every functor $F_{+}: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{D}}_{+}$, composition $\widetilde{G}$ induces an equivalence of $\infty $-categories
\[ \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+}) } \{ F_{+} \} \rightarrow \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{D}}_{-} )) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{-}) } \{ G \circ F_{+} \} . \]
Proof.
We first show that $(1) \Rightarrow (2)$. Let $\lambda = (\lambda _{-}, \lambda _{+}): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ be a coupling of $\infty $-categories and let $F_{-}: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{D}}_{-}$ and $F_{+}: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{D}}_{+}$ be functors. If condition $(1)$ is satisfied, then Remark 4.5.2.9 guarantees that the diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \ar [r]^-{\widetilde{G} \circ } \ar [d]^{\mu \circ } & \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{D}}_{-} ) ) \ar [d] \\ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} ) \times \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{+} ) \ar [r] & \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} ) \times \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{-} ) } \]
is a categorical pullback square, where the vertical maps are left fibrations (Corollary 4.2.5.2). Assertion $(2)$ now follows by applying Corollary 4.5.2.31 to the object $( F_{-}^{\operatorname{op}} \circ \lambda _{-}, F_{+} \circ \lambda _{+} ) \in \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} ) \times \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{+} )$. The implication $(2) \Rightarrow (3)$ follows by applying Corollary 5.1.6.4 to the commutative diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=-20pt{ \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+}) } \{ F_{+} \} \ar [rr] \ar [dr] & & \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{D}}_{-} )) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{-}) } \{ G \circ F_{+} \} \ar [dl] \\ & \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{D}}_{-} )^{\operatorname{op}}, & } \]
since the vertical maps are left fibrations (Proposition 8.2.2.2). We complete the proof by showing that $(3)$ implies $(1)$. Specializing assertion $(3)$ to the coupling $\lambda : \Delta ^0 \xrightarrow {\sim } (\Delta ^0)^{\operatorname{op}} \times \Delta ^0$, we deduce that $\widetilde{G}$ induces an equivalence of $\infty $-categories $\operatorname{\mathcal{D}}\times _{ \operatorname{\mathcal{D}}_{+} } \{ D\} \rightarrow \operatorname{Tw}( \operatorname{\mathcal{D}}_{-} ) \times _{ \operatorname{\mathcal{D}}_{-} } \{ G(D) \} $ for each object $D \in \operatorname{\mathcal{D}}_{+}$, so that (8.39) is a categorical pullback square by virtue of Proposition 8.2.3.7.
$\square$