Kerodon

Proof. To show that $V$ is a cocartesian fibration, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex (Proposition 5.1.4.8). In this case, $U$ is exponentiable (Corollary 9.4.6.19), so the desired result follows from Variant 8.6.5.11. To prove the second assertion, we may assume that $\operatorname{\mathcal{C}}= \Delta ^1$ with $C = 0$ and $C' = 1$. In this case, $\operatorname{\mathcal{E}}_{C}$ and $\operatorname{\mathcal{E}}_{C'}$ are full subcategories of $\operatorname{\mathcal{E}}$, and determine restriction functors $R: \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{D}})$ and $R': \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_{C'}, \operatorname{\mathcal{D}})$. The covariant transport functor $e_{!}$ can then be identified with the composition $R' \circ R^{L}$, where $R^{L}$ is left adjoint to $R$ (given by left Kan extension along the inclusion $\operatorname{\mathcal{E}}_{C} \hookrightarrow \operatorname{\mathcal{E}}$). Since the functor $R^{L}$ preserves all colimits (Corollary 7.1.4.22), we are reduced to showing that the functor $R'$ preserves $\kappa $-small colimits, which follows from the criterion of Proposition 7.1.7.3. $\square$

Proof. Fix an object $X \in \operatorname{\mathcal{E}}$ having image $C = U(X)$ and an edge $e$ of the $\infty $-category $\operatorname{\mathcal{C}}_{C/}$, which we identify with a $2$-simplex $\sigma :$

of $\operatorname{\mathcal{C}}$, and let $H_{e}: \operatorname{N}_{\bullet }( \{ C' < C'' \} ) \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be as in condition $(\ast )$ of Remark 9.4.8.5; we wish to show that the functor $F_{e}$ is left Kan extended from the subcategory $\{ C' \} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Without loss of generality, we may assume that $\operatorname{\mathcal{C}}= \Delta ^2$ and that $\sigma $ is the identity morphism. In this case, we can identify $F_{e}$ with the composition

where $\mathscr {F}$ is corepresented by the object $X \in \operatorname{\mathcal{E}}$. Since $U$ is flat, the desired result is a reformulation of Lemma 9.4.7.2. $\square$

Proof. Let us identify $H$ with a functor $F: \operatorname{\mathcal{E}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$. If $X$ an object of $\operatorname{\mathcal{E}}$ having image $C = U(X)$ and $u: C \rightarrow D$ is a morphism of $\operatorname{\mathcal{C}}$, our assumption that $U$ is a cocartesian fibration guarantees that we can lift $u$ to a $U$-cocartesian morphism $\widetilde{u}: X \rightarrow Y$ of $\operatorname{\mathcal{E}}$. In this case, we can identify $F(X,u)$ with a functor $\operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ which is corepresented by the object $Y$. It follows that $F$ factors through the full subcategory $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \subseteq \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ of Construction 8.6.5.6. Unwinding the definitions, we have a commutative diagram

Let $V: \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \rightarrow \operatorname{\mathcal{C}}$ and $V^{\dagger }: \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ denote the projection maps, and set $V^{\operatorname{corep}} = V|_{ \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) }$. Then the lower horizontal map exhibits $V^{\dagger }$ as a cartesian conjugate of $V$ (Proposition 8.6.2.3), and the upper horizontal map exhibits $U^{\operatorname{op}}$ as a cartesian conjugate of $V^{\operatorname{corep}}$ (Theorem 8.6.6.15). Moreover, the inclusion map $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \subseteq \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ exhibits $\operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ as a fiberwise $\kappa $-cocompletion of $\operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )$ (Example 9.4.2.5). Applying Proposition 9.4.3.3, we conclude that $h$ exhibits $\operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger }$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}^{\operatorname{op}}$. $\square$

Proof. Using Theorem 9.4.4.1, we can choose a diagram

which exhibits $\widehat{\operatorname{\mathcal{E}}}^{\operatorname{op}}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}^{\operatorname{op}}$. Since $U$ is flat, the inner fibration $U^{\operatorname{op}}$ is also flat (Remark 9.4.6.5). Applying the criterion of Proposition 9.4.6.9, we see that $\widehat{U}^{\operatorname{op}}$ is a cartesian fibration. Let $\lambda $ be a regular cardinal of exponential cofinality $\geq \kappa $ such that $\widehat{U}$ is essentially $\lambda $-small. Let $h^{+}$ denote the composition of $h$ with the inclusion functor

We will complete the proof by showing that $h^{+}$ is fully faithful.

Since $\lambda $ has exponential cofinality $\geq \kappa $, the $\infty $-category $\operatorname{\mathcal{S}}^{< \lambda }$ admits $\kappa $-small limits (Example 7.6.6.4). Let $\operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ denote the relative exponential of Construction 4.5.9.1. By definition, objects of $\operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ can be identified with pairs $(C, \mathscr {G} )$, where $C$ is an object of $\operatorname{\mathcal{C}}$ and $\mathscr {G}: \widehat{\operatorname{\mathcal{E}}}_{C} \rightarrow \operatorname{\mathcal{S}}^{< \lambda }$ is a functor. Let $\operatorname{Fun}'( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ be the full subcategory spanned by those pairs $(C, \mathscr {F} )$, where the functor $\mathscr {G}$ preserves $\kappa $-small limits. Let $\widehat{H}: \widehat{\operatorname{\mathcal{E}}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{S}}^{< \lambda }$ be a relative $\operatorname{Hom}$-functor for $\widehat{U}$, which we identify with a map

Since corepresentable functors preserve limits (Corollary 7.4.1.19), the functor $\widehat{h}$ factors through the full subcategory $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{Fun}'( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } ))$. Since $F$ is fully faithful (Remark 9.4.1.14), the functor $h^{+}$ is isomorphic to the composition

where $T$ is given by precomposition with $F$. It follows from the universal property of Theorem 9.4.1.20 that precomposition with $F$ induces an equivalence $\operatorname{Fun}'( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ of inner fibrations over $\operatorname{\mathcal{C}}$, so that $T$ is an equivalence of $\infty $-categories. To complete the proof, it will suffice to show that the functor $\widehat{h}$ is fully faithful. In other words, we can replace $U$ by $\widehat{U}$ (and $\kappa $ by the cardinal $\lambda $) and thereby reduce to proving Lemma 9.4.8.8 under the assumption that $U$ is a cocartesian fibration. In this case, the desired result follows from Lemma 9.4.8.7 (and Remark 9.4.1.14). $\square$

Proof of Theorem 9.4.8.4. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a flat inner fibration of $\infty $-categories which is essentially $\kappa $-small. It follows from Lemma 9.4.8.8 that a relative $\operatorname{Hom}$-functor for $U$ determines a fully faithful functor $h: \operatorname{\mathcal{E}}^{\operatorname{op}} \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa })^{\dagger }$. We wish to show that the diagram

exhibits $\operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger }$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}^{\operatorname{op}}$. By construction, $V^{\dagger }$ is a cartesian fibration which is conjugate to $V: \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \rightarrow \operatorname{\mathcal{C}}$. In particular, for every morphism $f: C \rightarrow C'$ of $\operatorname{\mathcal{C}}$, the contravariant transport functor

for the cartesian fibration $V^{\dagger }$ can be identified with the covariant transport functor

for the cocartesian fibration $V$ (see Proposition 8.6.1.5), and therefore preserves $\kappa $-small colimits (Lemma 9.4.8.2). By virtue of Proposition 9.4.1.16, it will suffice to show that for each object $C \in \operatorname{\mathcal{C}}$, the map of fibers

exhibits $\{ C\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\dagger }$ as a $\kappa $-cocompletion of $\operatorname{\mathcal{E}}_{C}^{\operatorname{op}}$. Unwinding the definitions, we see that the composition of $h_{C}$ with the equivalence

identifies with the contravariant Yoneda embedding for the $\infty $-category $\operatorname{\mathcal{E}}_{C}$. The desired result now follows from Theorem 8.4.3.3. $\square$