Kerodon

Proof. This is a special case of Corollary 5.1.2.3. $\square$

Proof. Let $\iota _0: \operatorname{\mathcal{E}}_0 \hookrightarrow \operatorname{\mathcal{E}}$ and $\iota _1: \operatorname{\mathcal{E}}_1 \hookrightarrow \operatorname{\mathcal{E}}$ denote the inclusion maps. Since $U$ is a cocartesian fibration, $\operatorname{\mathcal{E}}_1$ is a reflective subcategory of $\operatorname{\mathcal{E}}$ (Corollary 6.2.3.2). Let $L: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}_1$ be a $\operatorname{\mathcal{E}}_1$-reflection functor (Lemma 6.2.2.14). Without loss of generality, we may assume that the functor $F: \operatorname{\mathcal{E}}_{0} \rightarrow \operatorname{\mathcal{E}}_1$ factors as a composition $\operatorname{\mathcal{E}}_0 \xrightarrow {\iota _0} \operatorname{\mathcal{E}}\xrightarrow {L} \operatorname{\mathcal{E}}_1$ (Remark 6.2.3.3). Note that $L$ is a left adjoint to the inclusion $\iota _1: \operatorname{\mathcal{E}}_1 \hookrightarrow \operatorname{\mathcal{E}}$ (Proposition 6.2.2.15).

Suppose that $U$ is also a cartesian fibration, so that the subcategory $\operatorname{\mathcal{E}}_0 \subseteq \operatorname{\mathcal{E}}$ is coreflective (Corollary 6.2.3.2). Let $L': \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}_0$ be a $\operatorname{\mathcal{E}}_0$-coreflection functor (Corollary 6.2.3.2), so that $L'$ can be regarded as a right adjoint to $\iota _0$ (Proposition 6.2.2.15). Invoking Remark 6.2.1.8, we conclude that the composite functor $F = L \circ \iota _0$ has a right adjoint $G$, given by the composition $L' \circ \iota _1 = L'|_{\operatorname{\mathcal{E}}_1}$. Moreover, Remark 6.2.3.3 guarantees that $G: \operatorname{\mathcal{E}}_1 \rightarrow \operatorname{\mathcal{E}}_0$ is given by contravariant transport along $e$.

We now prove the converse. Suppose that the functor $F: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}_1$ admits a right adjoint $G: \operatorname{\mathcal{E}}_1 \rightarrow \operatorname{\mathcal{E}}_0$. Fix an object $Z \in \operatorname{\mathcal{E}}_1$; we wish to show that there exists an object $Y \in \operatorname{\mathcal{E}}_0$ and a $U$-cartesian morphism $f: Y \rightarrow Z$. Let $\epsilon : F \circ G \rightarrow \operatorname{id}_{\operatorname{\mathcal{E}}_1}$ be the counit of an adjunction between $F$ and $G$. Set $Y = G(Z)$, so that $\epsilon $ determines a morphism $\epsilon _{Z}: F(Y) \rightarrow Z$ in the $\infty $-category $\operatorname{\mathcal{E}}_1$. Let $\eta : \operatorname{id}_{\operatorname{\mathcal{E}}} \rightarrow L$ be a natural transformation which exhibits $L$ as a $\operatorname{\mathcal{E}}_1$-reflection functor, so that $\eta $ determines a morphism $\eta _{Y}: Y \rightarrow F(Y)$. Let $f: Y \rightarrow Z$ be a composition of $\eta _{Y}$ with $\epsilon _{Z}$. We will complete the proof by showing that $f$ is $U$-cartesian. To prove this, it will suffice to show that for every object $X \in \operatorname{\mathcal{E}}_0$, the composite map

is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$ (see Corollary 5.1.2.3). Unwinding the definitions, we see that this map factors as a composition

where the composition of the first two maps is an isomorphism in $\mathrm{h} \mathit{\operatorname{Kan}}$ because $\epsilon $ is the counit of an adjunction (see Proposition 6.2.1.17), and third is an isomorphism because $\eta _ X$ exhibits $F(X)$ as a $\operatorname{\mathcal{E}}_1$-reflection of $X$. $\square$

Proof. Assume first that condition $(1)$ is satisfied and let $e: C \rightarrow D$ be an edge of the simplicial set $\operatorname{\mathcal{C}}$, which we identify with a morphism $\Delta ^1 \rightarrow \operatorname{\mathcal{C}}$. Applying Proposition 6.2.3.4 to the projection map $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^1$, we deduce that the covariant transport functor $e_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ is right adjoint to the contravariant transport functor $e^{\ast } \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$, which proves $(2)$.

We now show that $(2)$ implies $(1)$. By virtue of Proposition 5.1.4.7, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex. For $0 \leq i \leq n$, let $\operatorname{\mathcal{E}}_{i}$ denote the fiber $\{ i\} \times _{\Delta ^ n} \operatorname{\mathcal{E}}$, which we regard as a full subcategory of $\operatorname{\mathcal{E}}$. We wish to show that, for every pair of integers $0 \leq j < k \leq n$ and every object $Z \in \operatorname{\mathcal{E}}_{k}$, there exists an object $Y \in \operatorname{\mathcal{E}}_{j}$ and a $U$-cartesian morphism $g: Y \rightarrow Z$ in $\operatorname{\mathcal{E}}$. Proposition 6.2.3.4 implies that the projection map $\operatorname{N}_{\bullet }( \{ j < k \} ) \times _{\Delta ^ n} \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }( \{ j < k \} )$ is a cartesian fibration, so we can choose an object $Y \in \operatorname{\mathcal{E}}_{j}$ and a morphism $g: Y \rightarrow Z$ which is locally $U$-cartesian. We will complete the proof by showing that $g$ is $U$-cartesian. To prove this, we must show that for each integer $0 \leq i \leq j$ and each object $W \in \operatorname{\mathcal{E}}_{i}$, composition with the homotopy class $[g]$ induces an isomorphism $\operatorname{Hom}_{\operatorname{\mathcal{E}}}( W, Y) \xrightarrow { [g] \circ } \operatorname{Hom}_{\operatorname{\mathcal{E}}}(W,Z)$ in the homotopy category of Kan complexes $\mathrm{h} \mathit{\operatorname{Kan}}$ (see Corollary 5.1.2.3). Since $U$ is a cocartesian fibration, we can choose a $U$-cocartesian morphism $f: W \rightarrow X$, where $X$ belongs to $\operatorname{\mathcal{E}}_{j}$. We conclude by observing that there is a commutative diagram

in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$, where the upper horizontal map is an isomorphism by virtue of our assumption that $g$ is locally $U$-cartesian, and the vertical maps are isomorphisms by virtue of our assumption that $f$ is $U$-cocartesian (Corollary 5.1.2.3). $\square$