Kerodon

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

Corollary 8.6.2.12. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. Suppose we are given cocartesian fibrations $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ and $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, a pair of cartesian fibrations $U^{\dagger }: \operatorname{\mathcal{D}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ and $V^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$, together with functors

\[ T_0: \operatorname{\mathcal{D}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{D}}\quad \quad T: \operatorname{\mathcal{E}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}} \]

which exhibit $U^{\dagger }$ and $V^{\dagger }$ as cartesian conjugates of $U$ and $V$, respectively. Then:

$(1)$

Precomposition with $T_0$ and postcomposition with $T$ induce fully faithful functors

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \xrightarrow {Q} \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{\mathcal{E}}) \xleftarrow {Q^{\dagger }} \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\operatorname{op}} }( \operatorname{\mathcal{D}}^{\dagger }, \operatorname{\mathcal{E}}^{\dagger } ). \]
$(2)$

Let $F$ be an object of $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$. Then $Q(F)$ belongs to the essential image of $Q^{\dagger }$ if and only if $F$ belongs to the full subcategory $\operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$ introduced in Notation 5.3.1.10 (that is, if and only if $F$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{D}}$ to $V$-cocartesian morphisms of $\operatorname{\mathcal{E}}$).

$(3)$

Let $F^{\dagger }$ be an object of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\operatorname{op}} }( \operatorname{\mathcal{D}}^{\dagger }, \operatorname{\mathcal{E}}^{\dagger } )$. Then $Q^{\dagger }( F^{\dagger } )$ belongs to the essential image of $Q$ if and only if $F^{\dagger }$ belongs to the full subcategory $\operatorname{Fun}^{\operatorname{Cart}}_{/\operatorname{\mathcal{C}}^{\operatorname{op}}}( \operatorname{\mathcal{D}}^{\dagger }, \operatorname{\mathcal{E}}^{\dagger })$ of Variant 5.3.1.11 (that is, if and only if $F^{\dagger }$ carries $U^{\dagger }$-cartesian morphisms of $\operatorname{\mathcal{D}}^{\dagger }$ to $V^{\dagger }$-cartesian morphisms of $\operatorname{\mathcal{E}}^{\dagger }$).

$(4)$

There is a canonical equivalence of $\infty $-categories $\Psi : \operatorname{Fun}_{/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\operatorname{op}} }^{\operatorname{Cart}}( \operatorname{\mathcal{D}}^{\dagger }, \operatorname{\mathcal{E}}^{\dagger } )$, which is characterized (up to isomorphism) by the requirement that the diagram

\[ \xymatrix { \operatorname{Fun}_{/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \ar [rr]^{\Psi } \ar [dr]^{\circ T_0} & & \operatorname{Fun}^{\operatorname{Cart}}_{/\operatorname{\mathcal{C}}^{\operatorname{op}}}( \operatorname{\mathcal{D}}^{\dagger }, \operatorname{\mathcal{E}}^{\dagger }) \ar [dl]_{T \circ } \\ & \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{\mathcal{E}}) & } \]

commutes up to isomorphism.

Proof. We will prove assertions $(1)$, $(2)$, and $(3)$; assertion $(4)$ is then a formal consequence. Applying Proposition 8.6.2.10 to $T_0$ we deduce that the functor $Q$ is fully faithful, and that its essential image is spanned by those objects $G \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{\mathcal{E}})$ which satisfy the following condition:

$(\ast )$

Let $w = (w',w'')$ be a morphism of $\operatorname{\mathcal{D}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}}} \operatorname{Tw}(\operatorname{\mathcal{C}})$. If $w'$ is $U^{\dagger }$-cartesian and $w''$ has degenerate image in $\operatorname{\mathcal{C}}$, then $G(w)$ is an isomorphism in $\operatorname{\mathcal{E}}$.

Applying Proposition 8.6.2.8 we see that $Q^{\dagger }$ is also fully faithful, and that its essential image consists of those $G$ which satisfy the following:

$(\ast ^{\dagger })$

Let $w = (w',w'')$ be a morphism of $\operatorname{\mathcal{D}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}}} \operatorname{Tw}(\operatorname{\mathcal{C}})$. If $w'$ is a degenerate edge of $\operatorname{\mathcal{D}}^{\dagger }$, then $G(w)$ is a $V$-cocartesian morphism of $\operatorname{\mathcal{E}}$.

This proves assertion $(1)$.

To prove $(2)$, we must show that an object $F \in \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{D}}$ to $V$-cocartesian morphisms of $\operatorname{\mathcal{E}}$ if and only if the induced map

\[ \operatorname{\mathcal{D}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \xrightarrow {T_0} \operatorname{\mathcal{D}}\xrightarrow {F} \operatorname{\mathcal{E}} \]

satisfies condition $(\ast ^{\dagger })$. The “only if” direction follows from our assumption that $T_0$ exhibits $U^{\dagger }$ as a cartesian conjugate of $U$. For the converse, assume that $Q(F) = F \circ T_0$ satisfies condition $(\ast ^{\dagger })$ and let $f: X \rightarrow Y$ be a $U$-cocartesian morphism of $\operatorname{\mathcal{D}}$, having image $e: C \rightarrow D$ in $\operatorname{\mathcal{C}}$. Choose an object $X' \in \operatorname{\mathcal{D}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ C \} $ such that $T_0(X')$ is isomorphic to $X$ as an object of the $\infty $-category $\{ C \} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$. Let $e_{L}: \operatorname{id}_{C} \rightarrow e$ be the morphism in $\operatorname{Tw}(\operatorname{\mathcal{C}})$ introduced in Example 8.1.3.6, and regard $w = (\operatorname{id}_{X'}, e_{L} )$ as an edge of $\operatorname{\mathcal{D}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$. Our assumption on $T_0$ guarantees that $T_0(w)$ is a $U$-cocartesian edge of $\operatorname{\mathcal{D}}$ lying over $e$, and is therefore isomorphic to $f$ (as an object of $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{D}})$). It will therefore suffice to show that $(F \circ T_0)(w)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$, which follows from condition $(\ast ^{\dagger })$.

To prove $(3)$, we must show that an object $F^{\dagger } \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\operatorname{op}} }( \operatorname{\mathcal{D}}^{\dagger }, \operatorname{\mathcal{E}}^{\dagger } )$ carries $U^{\dagger }$-cartesian morphisms of $\operatorname{\mathcal{D}}^{\dagger }$ to $V^{\dagger }$-cartesian morphisms of $\operatorname{\mathcal{E}}^{\dagger }$ if and only if the induced map

\[ \operatorname{\mathcal{D}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \xrightarrow {F^{\dagger } \times \operatorname{id}} \operatorname{\mathcal{E}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \xrightarrow {T} \operatorname{\mathcal{E}}. \]

satisfies condition $(\ast ^{\dagger })$. The “only if” direction follows immediately from our assumption that $T$ exhibits $V^{\dagger }$ as a cartesian conjugate of $V$, and the reverse implication follows from the criterion of Remark 8.6.1.14. $\square$