# Kerodon

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

Lemma 9.3.4.3. Let $\mathbb {K}$ be a collection of simplicial sets and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an isofibration of $\infty$-categories Then there exists a commutative diagram of $\infty$-categories

$\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}}$ (in the sense of Definition 9.3.1.12). Moreover, $\widehat{U}$ is also an isofibration.

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

$\operatorname{\mathcal{E}}\simeq \operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$

(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.8), 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.3.2.1, we deduce that there is 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}}'$. Moreover, the morphism $\widehat{U}'$ is a cocartesian fibration (and therefore an isofibration; see Proposition 5.1.4.8). Define $\widehat{\operatorname{\mathcal{E}}} \subseteq \widehat{\operatorname{\mathcal{E}}}'$ as in the statement of Lemma 9.3.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.3.4.2 guarantees that the diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^-{H'|_{\operatorname{\mathcal{E}}}} \ar [dr]_{U} & & \widehat{\operatorname{\mathcal{E}}} \ar [dl]^{ \widehat{U} } \\ & \operatorname{\mathcal{C}}& }$

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