Kerodon

Proof. Assume that $\operatorname{Tr}_{\operatorname{\mathcal{E}}^{\vee }/\operatorname{\mathcal{C}}}$ is isomorphic to $\sigma \circ \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$; we will show that $U^{\vee }$ is cocartesian dual to $U$ (the reverse implication then follows formally from the fact that cocartesian duals are unique up to equivalence; see Theorem 8.6.4.1). Let $\pi : \operatorname{QCat}^{\asymp } \rightarrow \operatorname{QCat}$ denote the forgetful functor, and let $\pi ': \operatorname{QCat}^{\asymp } \rightarrow \operatorname{QCat}$ be the composition of $\pi $ with the automorphism $\widetilde{\sigma }: \operatorname{QCat}^{\asymp } \simeq \operatorname{QCat}^{\asymp }$ described in Construction 8.6.7.6. By virtue of Proposition 8.6.7.5, we may assume without loss of generality that the covariant transport representation $\mathscr {F}_{+} = \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ factors as a composition $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\pi ) \circ \mathscr {F}$ for some diagram $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}^{\asymp }$. Set $\mathscr {F}_{-} = \operatorname{N}_{\bullet }^{\operatorname{hc}}(\pi ') \circ \mathscr {F}$. Our assumption then guarantees that $\mathscr {F}_{-}$ is a covariant transport representation for $U^{\vee }$. We may therefore assume without loss of generality that $U$ and $U^{\vee }$ coincide with the projection maps $\int _{\operatorname{\mathcal{C}}} \mathscr {F}_{+} \rightarrow \operatorname{\mathcal{C}}$ and $\int _{\operatorname{\mathcal{C}}} \mathscr {F}_{-} \rightarrow \operatorname{\mathcal{C}}$, respectively.

We now proceed as in the proof of Proposition 8.6.3.23. Define a simplicial functor $\tau : \operatorname{QCat}^{\asymp } \rightarrow \operatorname{QCat}$ as follows:

• On objects, $\tau $ is given by the construction $\operatorname{\mathcal{D}}\mapsto \operatorname{Tw}(\operatorname{\mathcal{D}})$.

• On morphism spaces, $\tau $ is given by the morphism of simplicial sets

  \begin{eqnarray*} \operatorname{Hom}_{ \operatorname{QCat}^{\asymp } }( \operatorname{\mathcal{D}}, \operatorname{\mathcal{D}}' )_{\bullet } & = & \operatorname{Tw}( \operatorname{Fun}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{D}}')^{\simeq } ) \\ & \rightarrow & \operatorname{Fun}( \operatorname{Tw}(\operatorname{\mathcal{D}}), \operatorname{Tw}(\operatorname{\mathcal{D}}') )^{\simeq } \\ & = & \operatorname{Hom}_{ \operatorname{QCat}}( \operatorname{Tw}(\operatorname{\mathcal{D}}), \operatorname{Tw}(\operatorname{\mathcal{D}}') )_{\bullet }. \end{eqnarray*}

  which classifies the composition

  \[ \operatorname{Tw}(\operatorname{\mathcal{D}}) \times \operatorname{Tw}( \operatorname{Fun}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{D}}')^{\simeq } ) \hookrightarrow \operatorname{Tw}(\operatorname{\mathcal{D}}\times \operatorname{Fun}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{D}}' ) ) \xrightarrow { \operatorname{Tw}(\operatorname{ev}) } \operatorname{Tw}(\operatorname{\mathcal{D}}'), \]

  where $\operatorname{ev}: \operatorname{\mathcal{D}}\times \operatorname{Fun}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{D}}' ) \rightarrow \operatorname{\mathcal{D}}'$ is the evaluation map.

Let $\widetilde{\mathscr {F}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ denote the diagram given by the composition $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \tau ) \circ \mathscr {F}$, and set $\widetilde{\operatorname{\mathcal{E}}} = \int _{\operatorname{\mathcal{C}}} \widetilde{\mathscr {F}}$. There is a natural transformation of simplicial functors $\tau \rightarrow \pi ' \times \pi $, which carries each $\infty $-category $\operatorname{\mathcal{D}}$ to the left fibration $\operatorname{Tw}(\operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{D}}^{\operatorname{op}} \times \operatorname{\mathcal{D}}$ of Proposition 8.1.1.11. Applying Corollary , see that this natural transformation induces a left fibration

We will complete the proof by showing that $\lambda $ exhibits $U^{\vee }$ as a cocartesian dual of $U$: that is, it satisfies conditions $(a)$ and $(b)$ of Definition 8.6.3.1.

$(a)$

Fix a vertex $C \in \operatorname{\mathcal{C}}$; we wish to show that the left fibration

\[ \lambda _{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \widetilde{\mathscr {F}} \rightarrow ( \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}_{-} ) \times ( \{ C \} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}_{+} ) \]

is a balanced coupling. Set $\operatorname{\mathcal{D}}= \widetilde{\mathscr {F}}(C)$. Using Example 5.6.2.18, we obtain a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}(\operatorname{\mathcal{D}}) \ar [r] \ar [d] & \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F} \ar [d]^{ \lambda _{C} } \\ \operatorname{\mathcal{D}}^{\operatorname{op}} \times \operatorname{\mathcal{D}}\ar [r] & ( \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}_{-} ) \times ( \{ C \} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}_{+} ), } \]

where the horizontal maps are equivalences of $\infty $-categories. The desired result now follows from the observation that the twisted arrow coupling $\operatorname{Tw}(\operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{D}}^{\operatorname{op}} \times \operatorname{\mathcal{D}}$ is balanced (Example 8.2.6.2).

$(b)$

Let $U: \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}$ denote the projection map, let $f: X \rightarrow X'$ be a $U$-cocartesian edge of $\widetilde{\operatorname{\mathcal{E}}}$, and let $\overline{f}: C \rightarrow C'$ denote the image of $f$ in the simplicial set $\operatorname{\mathcal{C}}$. The functor $\mathscr {F}$ carries the vertex $C$ to an $\infty $-category $\operatorname{\mathcal{D}}$, $C'$ to an $\infty $-category $\operatorname{\mathcal{D}}'$, and $\overline{f}$ to a vertex of the Kan complex $\operatorname{Tw}( \operatorname{Fun}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{D}}' )^{\simeq } )$, which we can identify with an isomorphism $u: F_{-} \rightarrow F_{+}$ between functors $F_{-}, F_{+}: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}'$. We can then identify $X$ with a morphism $e: D_{-} \rightarrow D_{+}$ in the $\infty $-category $\operatorname{\mathcal{D}}$ and $X'$ with a morphism $e': D'_{-} \rightarrow D'_{+}$ in the $\infty $-category $\operatorname{\mathcal{D}}'$, so that $f$ determines a morphism in the $\infty $-category $\operatorname{Tw}(\operatorname{\mathcal{D}}')$ which we depict informally in the diagram $\operatorname{\mathcal{D}}'$ which we depict informally in the diagram

\[ \xymatrix@R =50pt@C=50pt{ F_{-}( D_{-} ) \ar [d]^{ u(e) } & D'_{-} \ar [l] \ar [d]^{ e' } \\ F_{+}( D_{+} ) \ar [r] & D'_{+}. } \]

Our assumption that $X$ is universal for the coupling $\lambda _{C}$ guarantees that $e$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}$ (Example 8.2.1.5), so that the left vertical map is an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}'$. Our assumption that $f$ is $U$-cocartesian guarantees that the horizontal maps in the diagram are also isomorphisms (Remark 5.6.2.14). It follows that $e'$ is also an isomorphism in $\operatorname{\mathcal{D}}$, so that $X'$ is universal for the coupling $\lambda _{C'}$ as desired.