Kerodon

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

9.3.3 Fiberwise Cocompletion of Cartesian Fibrations

We now study fiberwise cocompletion in the setting of cartesian fibrations. Here the main result is the following:

Theorem 9.3.3.1. Let $\mathbb {K}$ be a collection of simplicial sets and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. Then a commutative diagram

9.39
$$\begin{gathered}\label{equation:fiberwise-cocompletion-cartesian-case} \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}}& } \end{gathered}$$

exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$ if and only if the following conditions are satisfied:

$(a)$

For each vertex $C \in \operatorname{\mathcal{C}}$, the functor $H_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \widehat{\operatorname{\mathcal{E}}}_{C}$ exhibits the $\infty$-category $\widehat{\operatorname{\mathcal{E}}}_{C}$ as a $\mathbb {K}$-cocompletion of the $\infty$-category $\operatorname{\mathcal{E}}_{C}$ (Definition 8.4.5.1).

$(b)$

The morphism $\widehat{U}$ is a cartesian fibration of simplicial sets.

$(c)$

For every edge $f: C \rightarrow C'$ of $\operatorname{\mathcal{C}}$, the contravariant transport functor $f^{\ast }: \widehat{\operatorname{\mathcal{E}}}_{C'} \rightarrow \widehat{\operatorname{\mathcal{E}}}_{C}$ preserves $K$-indexed colimits for each $K \in \mathbb {K}$.

$(d)$

The morphism $H$ carries $U$-cartesian edges of $\operatorname{\mathcal{E}}$ to $\widehat{U}$-cartesian edges of $\widehat{\operatorname{\mathcal{E}}}$.

Moreover, there exists a diagram (9.39) which satisfies these conditions.

Our strategy is to reduce Theorem 9.3.3.1 from its counterpart for cocartesian fibrations (Theorem 9.3.2.1), which was proved in ยง9.3.2. To carry out the reduction, we show that fiberwise cocompletion is compatible with the formation of conjugate fibrations (Proposition 9.3.3.3). As a first step, we record the easy direction of Theorem 9.3.3.1:

Lemma 9.3.3.2. Let $\mathbb {K}$ be a collection of simplicial sets, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration 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 satisfies the conditions of Theorem 9.3.3.1. Then $H$ exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$.

Proof. Without loss of generality, we may assume that $\operatorname{\mathcal{C}}= \Delta ^1$. For $i \in \{ 0,1\}$, let $\operatorname{\mathcal{E}}_{i}$ denote the fiber $\{ i\} \times _{\Delta ^1} \operatorname{\mathcal{E}}$ and define $\widehat{\operatorname{\mathcal{E}}}_{i}$ similarly, so that $H$ restricts to a functor $H_{i}: \operatorname{\mathcal{E}}_{i} \rightarrow \widehat{\operatorname{\mathcal{E}}}_{i}$. By assumption, the functor $H_{i}$ exhibits $\widehat{\operatorname{\mathcal{E}}}_{i}$ as a $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}_{i}$, and is therefore fully faithful (Proposition 8.4.5.3). Since $H$ carries $U$-cartesian morphisms of $\operatorname{\mathcal{E}}$ to $\widehat{U}$-cartesian morphisms of $\widehat{\operatorname{\mathcal{E}}}$, it follows that $H$ is fully faithful (Proposition 5.1.6.7). It follows from Example 9.3.1.6 that the fibration $\widehat{U}$ is $\mathbb {K}$-cocomplete.

Fix an uncountable regular cardinal $\kappa$ such that $\widehat{\operatorname{\mathcal{E}}}$ is locally $\kappa$-small and every simplicial set $K \in \mathbb {K}$ is essentially $\kappa$-small. To complete the proof, it will suffice to show that for every object $X \in \operatorname{\mathcal{E}}_{0}$, the functor

$\mathscr {F}: \widehat{\operatorname{\mathcal{E}}}_{1} \rightarrow \operatorname{\mathcal{S}}^{< \kappa } \quad \quad Y \mapsto \operatorname{Hom}_{\widehat{\operatorname{\mathcal{E}}} }( H(X), Y )$

commutes with $K$-indexed colimits, for each $K \in \mathbb {K}$. Since $\widehat{U}$ is a cartesian fibration, this functor factors as a composition $\widehat{\operatorname{\mathcal{E}}}_{1} \xrightarrow { f^{\ast } } \widehat{\operatorname{\mathcal{E}}}_0 \xrightarrow { \mathscr {G}} \operatorname{\mathcal{S}}^{< \kappa }$, where $f^{\ast }$ is given by contravariant transport along the nondegenerate edge of $\operatorname{\mathcal{C}}$ and the functor $\mathscr {G}$ is corepresented by $H(X)$. We are therefore reduced to showing that the functor $\mathscr {G}$ preserves $K$-indexed colimits, which follows from the recognition principle of Variant 8.4.6.9. $\square$

Proposition 9.3.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.40
$$\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}$$

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.41
$$\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}$$

satisfies the hypotheses of Theorem 9.3.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.3.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.10, 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.40) commutes up to isomorphism (moreover, $H^{\dagger }$ is unique up to isomorphism). We complete the proof by showing that the diagram (9.41) satisfies the conditions of Theorem 9.3.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.40), 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.3.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 Remark 8.6.2.11.

$\square$

Corollary 9.3.3.4. Let $\mathbb {K}$ be a collection of simplicial sets and let $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be a cartesian fibration of simplicial sets. Then there exists a diagram

9.42
$$\begin{gathered}\label{equation:fiberwise-completion-cocartesian-case-revisited} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger } \ar [rr]^-{H^{\dagger } } \ar [dr]_{U^{\dagger } } & & \widehat{\operatorname{\mathcal{E}}}^{\dagger } \ar [dl]^{ \widehat{U}^{\dagger } } \\ & \operatorname{\mathcal{C}}^{\operatorname{op}} & } \end{gathered}$$

which satisfies the conditions of Theorem 9.3.3.1.

Proof. Using Corollary 8.6.6.3, we can choose a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and a morphism $T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ which exhibits $U^{\dagger }$ as a cartesian conjugate of $U$. Applying Theorem 9.3.2.1, we can choose a 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}}$, where $\widehat{U}$ is a cocartesian fibration. Using Proposition 8.6.2.3, we can choose a cartesian fibration $\widehat{U}^{\dagger }: \widehat{\operatorname{\mathcal{E}}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ and a morphism $\widehat{T}: \widehat{\operatorname{\mathcal{E}}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \widehat{\operatorname{\mathcal{E}}}$ which exhibits $\widehat{U}^{\dagger }$ as a cartesian conjugate of $\widehat{U}$. The desired result now follows from Proposition 9.3.3.3. $\square$

Proof of Theorem 9.3.3.1. Let $\mathbb {K}$ be a collection of simplicial sets and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. Using Corollary 9.3.3.4, we can choose 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 satisfies the conditions of Theorem 9.3.3.1, and therefore exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$ (Lemma 9.3.3.2). Conversely, if we are given another diagram

9.43
$$\begin{gathered}\label{equation:proof-of-fiberwise-cocompletion2-cartesian} \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}}& } \end{gathered}$$

which exhibits $\widehat{\operatorname{\mathcal{E}}}'$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$, then Remark 9.3.1.21 guarantees that there is an equivalence $F: \widehat{\operatorname{\mathcal{E}}} \rightarrow \widehat{\operatorname{\mathcal{E}}}'$ of inner fibrations over $\operatorname{\mathcal{C}}$ such that $H'$ is isomorphic to $F \circ H$ as an object of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}}' )$. It then follows that (9.43) the conditions of Theorem 9.3.2.1. $\square$