Kerodon

Proof. Without loss of generality, we may assume that $\operatorname{\mathcal{C}}= \Delta ^1$; in this case, we must show that the diagram (9.47) satisfies conditions $(1)$ through $(4)$ of Definition 9.4.1.8. Condition $(1)$ follows from Corollary 8.4.6.10, and the remaining conditions follow immediately from the corresponding conditions on the diagram (9.46) $\square$

Proof. Choose a factorization of $U$ as a composition $\operatorname{\mathcal{E}}\xrightarrow {F} \operatorname{\mathcal{E}}' \xrightarrow {U'} \operatorname{\mathcal{C}}$, where $U'$ is a cocartesian fibration of $\infty $-categories and $F$ is fully faithful. For example, we can take $\operatorname{\mathcal{E}}'$ to be the oriented fiber product $\operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$, $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be the projection onto the second factor (which is a cocartesian fibration by virtue of Corollary 5.3.7.3), and $F$ to be the inclusion map

(which is fully faithful by virtue of Corollary 4.5.2.22). Let $\operatorname{\mathcal{E}}'_0 \subseteq \operatorname{\mathcal{E}}'$ be the essential image of $F$. Since $U'$ is an isofibration (Proposition 5.1.4.9), it restricts to an isofibration $\operatorname{\mathcal{E}}'_0 \rightarrow \operatorname{\mathcal{C}}$. Applying Proposition 5.1.7.5, we see that the functor $F: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'_0$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}$. We may therefore replace $\operatorname{\mathcal{E}}$ by $\operatorname{\mathcal{E}}'_0$ and thereby reduce to the special case where $\operatorname{\mathcal{E}}$ is a replete full subcategory of $\operatorname{\mathcal{E}}'$.

Applying Theorem 9.4.2.1, we deduce that there is a commutative diagram

which exhibits $\widehat{\operatorname{\mathcal{E}}}'$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}'$. Moreover, the morphism $\widehat{U}'$ is a cocartesian fibration (and therefore an isofibration; see Proposition 5.1.4.9). Define $\widehat{\operatorname{\mathcal{E}}} \subseteq \widehat{\operatorname{\mathcal{E}}}'$ as in the statement of Lemma 9.4.4.2. Then $\widehat{\operatorname{\mathcal{E}}}$ is a replete full subcategory of $\widehat{\operatorname{\mathcal{E}}}'$, so the restriction map $\widehat{U} = \widehat{U}'|_{\widehat{\operatorname{\mathcal{E}}} }$ is an isofibration. Moreover, Lemma 9.4.4.2 guarantees that the diagram

exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. $\square$

Proof. Using Proposition 1.1.4.12, we can reduce to the case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex and $\operatorname{\mathcal{C}}_0 = \operatorname{\partial \Delta }^ n$ is its boundary. In this case, $U$ is an isofibration of $\infty $-categories (Example 4.4.1.6). Applying Lemma 9.4.4.3, we deduce that there exists a diagram

which exhibits $\widehat{\operatorname{\mathcal{E}}}'$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. Set $\widehat{\operatorname{\mathcal{E}}}'_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}$, so that $H'_0 = H'|_{\operatorname{\mathcal{E}}_0}$ exhibits $\widehat{\operatorname{\mathcal{E}}}'_0$ as a fiberwise $\mathbb {K}$-completion of $\operatorname{\mathcal{E}}_0$. Applying Remark 9.4.1.21, we deduce that there exists an isomorphism $H'_0 \simeq F_0 \circ H_0$ in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}'_0 )$, where $F_0: \widehat{\operatorname{\mathcal{E}}}_0 \rightarrow \widehat{\operatorname{\mathcal{E}}}'_0$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}_0$. Using Lemma 5.6.7.1, we can choose an inner fibration $\widehat{U}: \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}$ and an equivalence $F: \widehat{\operatorname{\mathcal{E}}} \rightarrow \widehat{\operatorname{\mathcal{E}}}'$ satisfying $F_0 = F|_{\widehat{\operatorname{\mathcal{E}}}_0}$. Composition with $F$ induces an equivalence of $\infty $-categories $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}}' )$. We can therefore choose a functor $H: \operatorname{\mathcal{E}}\rightarrow \widehat{\operatorname{\mathcal{E}}}$ such that $F \circ H$ is isomorphic to $H'$ in the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}}' )$. It follows that $F_0 \circ H|_{ \operatorname{\mathcal{E}}_0 }$ is isomorphic to $F_0 \circ H_0$ as objects of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}'_0 )$. Since $F_0$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}_0$, it follows that $H_0$ and $H|_{\operatorname{\mathcal{E}}_0}$ are isomorphic as objects of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}_0 )$. Since the restriction functor $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}_0 )$ is an isofibration (Proposition 4.1.4.1), we can arrange (after replacing $H$ by an isomorphic functor if necessary) that $H|_{\operatorname{\mathcal{E}}_0} = H_0$. We conclude by observing that the diagram

exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. $\square$

Proof of Theorem 9.4.4.1. Apply Lemma 9.4.4.4 in the special case $\operatorname{\mathcal{C}}_0 = \emptyset $. $\square$