Proposition 9.4.3.3. Let $\mathbb {K}$ be a collection of simplicial sets, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $\widehat{U}: \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets, and suppose we are given a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^-{H} \ar [dr]_{U} & & \widehat{\operatorname{\mathcal{E}}} \ar [dl]^{ \widehat{U} } \\ & \operatorname{\mathcal{C}}& } \]
which exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. Let $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ and $\widehat{U}^{\dagger }: \widehat{\operatorname{\mathcal{E}}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be cartesian fibrations, and let
\[ T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}\quad \quad \widehat{T}: \widehat{\operatorname{\mathcal{E}}}^{\dagger } \times _{ \operatorname{\mathcal{C}}}^{\operatorname{op}} \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \widehat{\operatorname{\mathcal{E}}} \]
be morphisms which exhibit $U^{\dagger }$ and $\widehat{U}^{\dagger }$ as cartesian conjugates of $U$ and $\widehat{U}$, respectively. Then there exists a morphism $H^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \widehat{\operatorname{\mathcal{E}}}^{\dagger }$ satisfying $\widehat{U}^{\dagger } \circ H^{\dagger } = U^{\dagger }$, and for which the diagram
9.42
\begin{equation} \begin{gathered}\label{equation:cocompletion-commutes-with-conjugate-fibrations} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [d]^{H^{\dagger } \times \operatorname{id}} \ar [r]^-{ T} & \operatorname{\mathcal{E}}\ar [d]^{H} \\ \widehat{\operatorname{\mathcal{E}}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [r]^-{ \widehat{T} } & \widehat{\operatorname{\mathcal{E}}} } \end{gathered} \end{equation}
commutes up to isomorphism (in the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}), \widehat{\operatorname{\mathcal{E}}} )$). In this case, the diagram
9.43
\begin{equation} \begin{gathered}\label{equation:cocompletion-commutes-with-conjugate-fibrations0} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger } \ar [dr]_{ U^{\dagger } } \ar [rr]^-{H^{\dagger } } & & \widehat{\operatorname{\mathcal{E}}}^{\dagger } \ar [dl]^{ \widehat{U}^{\dagger } } \\ & \operatorname{\mathcal{C}}^{\operatorname{op}} & } \end{gathered} \end{equation}
satisfies the hypotheses of Theorem 9.4.3.1, and therefore exhibits $\widehat{\operatorname{\mathcal{E}}}^{\dagger }$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}^{\dagger }$.
Proof.
By virtue of Corollary 5.6.7.3, we may assume that $\operatorname{\mathcal{C}}$ is an $\infty $-category. It follows from the criterion of Theorem 9.4.2.1 that the functor $H$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{E}}$ to $\widehat{U}$-cocartesian morphisms of $\widehat{\operatorname{\mathcal{E}}}$. Invoking Example 8.6.2.13, we deduce that there is an object $H^{\dagger } \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\operatorname{op}} }( \operatorname{\mathcal{E}}^{\dagger }, \widehat{\operatorname{\mathcal{E}}}^{\dagger } )$ for which the diagram (9.42) commutes up to isomorphism (moreover, $H^{\dagger }$ is unique up to isomorphism). We complete the proof by showing that the diagram (9.43) satisfies the conditions of Theorem 9.4.3.1:
- $(a)$
Fix an object $C \in \operatorname{\mathcal{C}}$; we wish to show that the functor $H^{\dagger }_{C}$ exhibits the $\infty $-category $\widehat{\operatorname{\mathcal{E}}}^{\dagger }_{C}$ as a $\mathbb {K}$-cocompletion of the $\infty $-category $\operatorname{\mathcal{E}}^{\dagger }_{C}$. Using (9.42), we obtain a diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger }_{C} \ar [r]^-{T_ C} \ar [d]^{ H^{\dagger }_{C} } & \operatorname{\mathcal{E}}_{C} \ar [d]^{H_ C } \\ \widehat{\operatorname{\mathcal{E}}}^{\dagger }_{C} \ar [r]^-{ \widehat{T}_{C} } & \widehat{\operatorname{\mathcal{E}}}_{C} } \]
which commutes up to isomorphism, where the horizontal maps are equivalences. The desired result now follows from our assumption that $H_{C}$ exhibits the $\infty $-category $\widehat{\operatorname{\mathcal{E}}}_{C}$ as a $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}_{C}$.
- $(b)$
The morphism $\widehat{U}^{\dagger }$ is a cartesian fibration by assumption.
- $(c)$
Fix a morphism $f: C \rightarrow C'$ of $\operatorname{\mathcal{C}}$ and a simplicial set $K \in \mathbb {K}$; we wish to show that the contravariant transport functor $f^{\ast }: \widehat{\operatorname{\mathcal{E}}}^{\dagger }_{C} \rightarrow \widehat{\operatorname{\mathcal{E}}}^{\dagger }_{C'}$ preserves $K$-indexed colimits. Proposition 8.6.1.5 then guarantees that the diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \widehat{\operatorname{\mathcal{E}}}^{\dagger }_{C} \ar [r]^-{ f^{\ast } } \ar [d]^{ \widehat{T}_{C} } & \widehat{\operatorname{\mathcal{E}}}^{\dagger }_{C'} \ar [d]^{ \widehat{T}_{C'} } \\ \widehat{\operatorname{\mathcal{E}}}_{C} \ar [r]^-{ f_{!} } & \widehat{\operatorname{\mathcal{E}}}_{C'} } \]
commutes up to isomorphism, where $f_{!}$ is given by covariant transport along $f$ for the cocartesian fibration $\widehat{U}$. Since the vertical maps are equivalences of $\infty $-categories, we are reduced to proving that the functor $f_{!}$ preserves $K$-indexed colimits, which follows from Theorem 9.4.2.1.
- $(d)$
The morphism $H^{\dagger }$ carries $U^{\dagger }$-cartesian edges of $\operatorname{\mathcal{E}}^{\dagger }$ to $\widehat{U}^{\dagger }$-cartesian edges of $\widehat{\operatorname{\mathcal{E}}}^{\dagger }$: this follows from Example 8.6.2.13.
$\square$