Kerodon

Proof. The implications $(1) \Rightarrow (2) \Rightarrow (3) \Rightarrow (4)$ are immediate from the definitions (see Corollary 9.4.5.9), and the implication $(4) \Rightarrow (1)$ is a reformulation of Theorem 9.4.6.6. $\square$

Proof. Using Corollary 5.6.7.3, we can reduce to the case where $\operatorname{\mathcal{C}}$ is an $\infty $-category. Fix objects $C, C' \in \operatorname{\mathcal{C}}$ such that $C$ is a retract of $C'$, and assume that $F_{C'}$ preserves $K$-indexed colimits; we wish to show that $F_{C}$ also preserves $K$-indexed colimits. Choose a colimit diagram $\overline{u}: K^{\triangleright } \rightarrow \widehat{\operatorname{\mathcal{E}}}_{C}$; we will show that $F_{C} \circ \overline{u}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{D}}$. Set $u = \overline{u}|_{K}$. It follows from Theorem 5.2.1.1 that $\widehat{U}$ induces a cartesian fibration $\operatorname{Fun}( K, \widehat{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$. Applying Remark 8.5.1.23, we deduce that there is a diagram $u': K \rightarrow \widehat{\operatorname{\mathcal{E}}}_{C'}$ having the property that $u$ is a retract of $u'$ in the $\infty $-category $\operatorname{Fun}(K, \widehat{\operatorname{\mathcal{E}}} )$. Since $\widehat{\operatorname{\mathcal{E}}}_{C'}$ admits $K$-indexed colimits, we can extend $u'$ to a colimit diagram $\overline{u}': K^{\triangleright } \rightarrow \widehat{\operatorname{\mathcal{E}}}_{C'}$. Since $\widehat{U}$ is a cartesian fibration, $\overline{u}$ and $\overline{u}'$ are $\widehat{U}$-colimit diagrams in the $\infty $-category $\widehat{\operatorname{\mathcal{E}}}$ (Corollary 7.3.3.23). Using Theorem 7.3.6.14, we see that any diagram which exhibits $u$ as a retract of $u'$ can be extended to a diagram which exhibits $\overline{u}$ as a retract of $\overline{u}'$. It follows that $F_{C} \circ \overline{u}$ is a retract of $F_{C'} \circ \overline{u}'$ (in the $\infty $-category $\operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{D}})$). Consequently, to show that $F_{C} \circ \overline{u}$ is a colimit diagram in $\operatorname{\mathcal{D}}$, it will suffice to show that $F_{C'} \circ \overline{u}'$ is a colimit diagram in $\operatorname{\mathcal{D}}$ (Corollary 8.5.1.12). This follows from our assumption that $F_{C'}$ preserves $K$-indexed colimits. $\square$

Proof. Set $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ and $\widehat{\operatorname{\mathcal{E}}}' = \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}$, so that $\overline{F}$ induces projection maps $F: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ and $\widehat{F}: \widehat{\operatorname{\mathcal{E}}}' \rightarrow \widehat{\operatorname{\mathcal{E}}}$. We wish to show that, for every idempotent complete $\infty $-category $\operatorname{\mathcal{D}}$, precomposition with $F$ induces an equivalence of $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{D}})$. By virtue of Proposition 9.4.5.10, we may assume without loss of generality that $\operatorname{\mathcal{D}}$ is $\kappa $-cocomplete (in fact, we can assume that $\operatorname{\mathcal{D}}= \operatorname{\mathcal{S}}^{< \lambda }$ for some uncountable regular cardinal $\lambda \geq \kappa $). Let $\operatorname{Fun}^{\kappa }( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}})$ denote the full subcategory of $\operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}})$ spanned by those diagrams $G: \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{D}}$ having the property that, for each vertex $C \in \operatorname{\mathcal{C}}$, the functor $G_{C} = G|_{ \widehat{\operatorname{\mathcal{E}}}_{C} }$ preserves $\kappa $-small colimits, and define $\operatorname{Fun}^{\kappa }( \widehat{\operatorname{\mathcal{E}}}', \operatorname{\mathcal{D}}) \subseteq \operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}})$ similarly. We then have a commutative diagram of $\infty $-categories

where the vertical maps are equivalences by virtue of the universal property of fiberwise $\kappa $-cocompletions (Theorem 9.4.1.20). It will therefore suffice to show that precomposition with $\widehat{F}$ induces an equivalence of $\infty $-categories $\operatorname{Fun}^{\kappa }( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}^{\kappa }( \widehat{\operatorname{\mathcal{E}}}', \operatorname{\mathcal{D}})$. Since $\overline{F}$ is a Morita equivalence and $\widehat{U}$ is a cartesian fibration, the morphism $\widehat{F}$ is also a Morita equivalence (Proposition 9.4.5.11). In particular, precomposition with $\widehat{F}$ induces an equivalence of $\infty $-categories $\operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}}', \operatorname{\mathcal{D}})$. To complete the proof, it will suffice to show that an object $G \in \operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}})$ belongs to the subcategory $\operatorname{Fun}^{\kappa }( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}})$ if and only if $G \circ \widehat{F}$ belongs to $\operatorname{Fun}^{\kappa }( \widehat{\operatorname{\mathcal{E}}}', \operatorname{\mathcal{D}})$. This follows from Lemma 9.4.6.11. $\square$

Proof. The implication $(2) \Rightarrow (1)$ follows from Lemma 9.4.6.12 and Corollary 9.4.5.9. Conversely, suppose that condition $(1)$ is satisfied. Set $\operatorname{\mathcal{E}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{E}}$ and $\widehat{\operatorname{\mathcal{E}}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \widehat{\operatorname{\mathcal{E}}}$. Using Proposition 5.6.7.2, we can choose a pullback diagram

where $\widehat{U}'$ is a cartesian fibration. Let us abuse notation by identifying $\widehat{\operatorname{\mathcal{E}}}_0$ with its image in $\widehat{\operatorname{\mathcal{E}}}'$. It follows from Proposition 5.3.6.1 that the inclusion map $\widehat{\operatorname{\mathcal{E}}}_0 \hookrightarrow \widehat{\operatorname{\mathcal{E}}}'$ is a categorical equivalence of simplicial sets, so there exists a functor $F: \widehat{\operatorname{\mathcal{E}}}' \rightarrow \widehat{\operatorname{\mathcal{E}}}$ which is the identity on $\widehat{\operatorname{\mathcal{E}}}_0$. We will complete the proof by showing that $F$ is an equivalence of inner fibrations over $\Delta ^2$, so that $\widehat{U}$ is also a cartesian fibration (Proposition 5.1.7.14).

Note that the inner $\widehat{U}$ and $\widehat{U}'$ are $\kappa $-cocomplete. It will therefore suffice to show that, for every $\kappa $-cocomplete inner fibration $V: \operatorname{\mathcal{D}}\rightarrow \Delta ^2$, precomposition with $F$ induces an equivalence of $\infty $-categories

Since the inclusion $\widehat{\operatorname{\mathcal{E}}}_0 \hookrightarrow \widehat{\operatorname{\mathcal{E}}}'$ is a categorical equivalence, this is equivalent to the statement that the restriction map

is an equivalence, where $\operatorname{\mathcal{D}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{D}}$. Invoking the universal property of fiberwise cocompletion (Theorem 9.4.1.20), we are reduced to showing that the restriction map $\operatorname{Fun}_{ / \Delta ^2 }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}_{ / \Delta ^2 }( \Lambda ^{2}_{1} \times _{\Delta ^2}, \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$ is an equivalence of $\infty $-categories, which follows immediately from assumption $(1)$. $\square$

Proof of Proposition 9.4.6.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially $\kappa $-small inner fibration and let

be a diagram which exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}$. It follows from Corollary 5.1.5.11 that $\widehat{U}$ is a cartesian fibration if and only if, for every $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$, the projection map $\widehat{U}_{\sigma }: \Delta ^2 \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}} \rightarrow \Delta ^2$ is a cartesian fibration. By virtue of Lemma 9.4.6.13, this is equivalent to the requirement that $U$ is flat. $\square$

Proof of Theorem 9.4.6.6. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a flat inner fibration of simplicial sets and let $\operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$ be a Morita equivalence; we wish to show that the projection map $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}$ is also a Morita equivalence. Choose an uncountable regular cardinal $\kappa $ such that $U$ is essentially $\kappa $-small. Using Theorem 9.4.4.1, we can choose a diagram

which exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}$. By virtue of Lemma 9.4.6.12, it will suffice to show that $\widehat{U}$ is a cartesian fibration, which is a reformulation of our assumption that $U$ is flat (Proposition 9.4.6.9). $\square$

Proof. Choose an uncountable regular cardinal $\kappa $ for which $\operatorname{\mathcal{E}}$ is essentially $\kappa $-small. Using Theorem 9.4.4.1, we can choose a diagram

which exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}$. It follows from Proposition 9.4.1.11 that $\widehat{U}$ is a cartesian fibration, so that $U$ is flat by virtue of Proposition 9.4.6.9. $\square$

Proof. Assume that $U$ is a flat isofibration; we will show that $U$ is exponentiable (the converse follows from Remark 4.5.9.12 and Example 9.4.6.2). Suppose we are given a commutative diagram of simplicial sets

in which both squares are pullbacks, where $\overline{F}$ is a categorical equivalence; we wish to show that $F$ is also a categorical equivalence. Using Proposition 4.1.3.2, we can factor $\overline{G}$ as a composition $\operatorname{\mathcal{C}}_0 \xrightarrow {\iota _0} \operatorname{\mathcal{C}}_{0}^{+} \xrightarrow {V_0} \operatorname{\mathcal{C}}$, where $\iota _0$ is inner anodyne and $V_0$ is an inner fibration. In particular, $\operatorname{\mathcal{C}}^{+}_{0}$ is an $\infty $-category. Replacing $\operatorname{\mathcal{C}}$ by $\operatorname{\mathcal{C}}^{+}_{0}$ (and $U$ by the projection map $\operatorname{\mathcal{C}}_0^{+} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}^{+}_{0}$), we can assume that $\overline{G}$ is inner anodyne. In this case, Corollary 9.4.6.7 guarantees that $G$ is a categorical equivalence of simplicial sets. It will therefore suffice to show that the composition $(G \circ F): \operatorname{\mathcal{E}}_1 \rightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence. Applying Proposition 4.1.3.2 again, we can factor $\overline{G} \circ \overline{F}$ as a composition $\operatorname{\mathcal{C}}_1 \xrightarrow {\iota _1} \operatorname{\mathcal{C}}_{1}^{+} \xrightarrow {V_{1}} \operatorname{\mathcal{C}}$, where $\iota _1$ is inner anodyne and $V_1$ is an inner fibration. Applying Corollary 9.4.6.7 again, we conclude that the inclusion map $\operatorname{\mathcal{E}}_1 \hookrightarrow \operatorname{\mathcal{C}}_{1}^{+} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is a categorical equivalence of simplicial sets. We are therefore reduced to showing that the projection map $\operatorname{\mathcal{C}}_{1}^{+} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}$ is an equivalence of $\infty $-categories. Note that $\overline{F}$, $\overline{G}$, and $\iota _{1}$ are categorical equivalences of simplicial sets, so the inner fibration $V_1$ is an equivalence of $\infty $-categories. The desired result now follows from Corollary 4.5.2.29 (since $U$ is an isofibration). $\square$

Proof. Combine Proposition 9.4.6.17 with Example 4.4.1.6. $\square$

Proof of Lemma 9.4.6.20. We will prove $(1)$; assertion $(2)$ then follows from Example 9.4.6.10. Using Corollary 4.5.2.23, we can factor the inclusion map $\{ C\} \hookrightarrow \operatorname{\mathcal{C}}$ as a composition $\{ C\} \hookrightarrow \widetilde{\operatorname{\mathcal{C}}} \xrightarrow {V} \operatorname{\mathcal{C}}$, where $V$ is an isofibration and $\widetilde{\operatorname{\mathcal{C}}}$ is a contractible Kan complex. Set $\widetilde{\operatorname{\mathcal{E}}} = \widetilde{\operatorname{\mathcal{C}}} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ and $\widetilde{\operatorname{\mathcal{E}}}' = \widetilde{\operatorname{\mathcal{C}}} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$, so that we have a commutative diagram of $\infty $-categories

It follows from Theorem 9.4.6.6 that the vertical maps are Morita equivalences, and from Corollary 4.5.2.29 that $\widetilde{F}$ is an equivalence of $\infty $-categories. Applying Remark 9.4.5.5, we conclude that $F_{C}$ is a Morita equivalence. $\square$

Proof. Combine Corollary 4.5.2.23 with Lemma 9.4.6.20. $\square$

Proof. Using Proposition 9.4.6.22, we can factor $U$ as a composition $\operatorname{\mathcal{E}}\xrightarrow {F} \operatorname{\mathcal{E}}' \xrightarrow {U'} \operatorname{\mathcal{C}}$, where $F$ is an equivalence of $\infty $-categories and $U'$ is an isofibration. For each object $C \in \operatorname{\mathcal{C}}$, Lemma 9.4.6.20 guarantees that the induced map $F_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}'_{C}$ is a Morita equivalence; in particular, every object of $\operatorname{\mathcal{E}}'_{C}$ is a retract of $F(X)$, for some object $X \in \operatorname{\mathcal{E}}_{C}$ (see Proposition 9.4.5.8). Since $\operatorname{\mathcal{E}}_{C}$ is idempotent complete, it follows that $F_{C}$ is an equivalence of $\infty $-categories. Applying Corollary 5.1.7.10, we conclude that $F$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}$, so that $U$ is also an isofibration (Proposition 5.1.7.14). $\square$

Proof. Choose an uncountable regular cardinal $\kappa $ for which the inner fibration $U_0$ is essentially $\kappa $-small. Using Theorem 9.4.4.1, we can choose a commutative diagram

which exhibits $\widehat{\operatorname{\mathcal{E}}}_0$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}_0$. Let $\operatorname{\mathcal{E}}'_0$ be the full simplicial subset of $\widehat{\operatorname{\mathcal{E}}}_0$ spanned by those vertices which belong to the image of $H_0$. It follows from Remark 9.4.1.15 that $H_0$ induces an equivalence $\operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}'_0$ of inner fibrations over $\operatorname{\mathcal{C}}_0$. Using Lemma 5.6.7.1 (and Remark 9.4.6.3), we can replace $\operatorname{\mathcal{E}}_0$ by $\operatorname{\mathcal{E}}'_0$ and thereby reduce to the case where $H_0$ is an isomorphism from $\operatorname{\mathcal{E}}_0$ onto a full simplicial subset of $\widehat{\operatorname{\mathcal{E}}}_0$.

Since $U_0$ is flat, the morphism $\widehat{U}_0$ is a cartesian fibration (Proposition 9.4.6.9). Using Proposition 5.6.7.2, we can choose a pullback diagram

where $\widehat{U}$ is a cartesian fibration. Let $\operatorname{Tr}_{\widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} \rightarrow \mathrm{h} \mathit{\operatorname{\mathcal{QC}}}$ be the homotopy transport representation of $\widehat{U}$. Since $\iota $ induces an isomorphism of homotopy categories $\mathrm{h} \mathit{ \operatorname{\mathcal{C}}_0 } \xrightarrow {\sim } \mathrm{h} \mathit{\operatorname{\mathcal{C}}}$, Proposition 9.4.1.16 guarantees that the functor $\operatorname{Tr}_{\widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}}$ carries each object of $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ to a $\kappa $-cocomplete $\infty $-category and each morphism of $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ to a functor which preserves $\kappa $-small colimits.

Let $\operatorname{\mathcal{E}}\subseteq \widehat{\operatorname{\mathcal{E}}}$ be the full simplicial subset spanned by those vertices which belong to the image of $\operatorname{\mathcal{E}}_0$, and set $U = \widehat{U}|_{\operatorname{\mathcal{E}}}$. Applying the criterion of Proposition 9.4.1.16, we see that the diagram

exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}$. Since $\widehat{U}$ is a cartesian fibration, Proposition 9.4.6.9 guarantees that the inner fibration $U$ is flat. By construction, the isomorphism $\widehat{\operatorname{\mathcal{E}}}_0 \xrightarrow {\sim } \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}$ restricts to an isomorphism of $\operatorname{\mathcal{E}}_0$ with the fiber product $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. $\square$

Proof. Combine Corollaries 9.4.6.26 and 9.4.6.23. $\square$

Proof. It follows from Example 9.4.6.10 that $\widehat{U}$ is a flat inner fibration. Since the fibers of $\widehat{U}$ are idempotent complete, it is an isofibration (Corollary 9.4.6.27). $\square$

Proof. Using Corollary 9.4.6.26, we can choose an inner anodyne map $\iota : \operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ and a pullback diagram

where $U'$ is a flat isofibration. Using Proposition 9.4.6.22, we can factor $U'$ as a composition $\operatorname{\mathcal{E}}' \xrightarrow {F} \operatorname{\mathcal{E}}'' \xrightarrow {U''} \operatorname{\mathcal{C}}$, where $F$ is an equivalence of $\infty $-categories and $U''$ is a flat isofibration. Set $\operatorname{\mathcal{E}}''_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}''$, so that we have a commutative diagram

Since $U'$ and $U''$ are flat, Proposition 9.4.6.6 guarantees that the horizontal maps are categorical equivalences. Since $F$ is an equivalence of $\infty $-categories, it follows that $F_0$ is a categorical equivalence of simplicial sets (Remark 4.5.3.5), and therefore an equivalence of isofibrations over $\operatorname{\mathcal{C}}_0$ (Proposition 5.1.7.5). Applying Lemma 5.6.7.1, we conclude that there exists a commutative diagram

where the left square is a pullback, the upper horizontal composition is $F_0$, and $G$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}$. Since $U''$ is a flat isofibration, it follows that $U$ is also a flat isofibration (Remark 9.4.6.3 and Proposition 5.1.7.14). $\square$

Proof. By virtue of Proposition 9.4.6.29, we may assume that $\operatorname{\mathcal{C}}$ is an $\infty $-category. In this case, the result follows from Proposition 9.4.6.17. $\square$