# Kerodon

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

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

9.33
$$\begin{gathered}\label{equation:fiberwise-cocompletion-cocartesian-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 cocartesian fibration of simplicial sets.

$(c)$

For every edge $f: C \rightarrow C'$ of $\operatorname{\mathcal{C}}$, the covariant transport functor $f_{!}: \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$-cocartesian edges of $\operatorname{\mathcal{E}}$ to $\widehat{U}$-cocartesian edges of $\widehat{\operatorname{\mathcal{E}}}$.

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

Proof of Theorem 9.3.2.1. Let $\mathbb {K}$ be a collection of simplicial sets and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Using Lemma 9.3.2.6, we can choose a commutative diagram

9.37
$$\begin{gathered}\label{equation:proof-of-fiberwise-cocompletion} \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 satisfies conditions $(a)$, $(b)$, $(c)$, and $(d)$ of Theorem 9.3.2.1. Lemma 9.3.2.3 guarantees any such diagram (9.37) exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. Conversely, if we are given another diagram

9.38
$$\begin{gathered}\label{equation:proof-of-fiberwise-cocompletion2} \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.38) also satisfies conditions $(a)$, $(b)$, $(c)$, and $(d)$ of Theorem 9.3.2.1. $\square$