Proposition 8.6.2.8. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration, and let $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be a cartesian fibration. Suppose we are given a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [rr]^{ T } \ar [dr] & & \operatorname{\mathcal{E}}\ar [dl]^{ U } \\ & \operatorname{\mathcal{C}}, & } \]
which we identify with a functor $F: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$. The following conditions are equivalent:
- $(a)$
The functor $T$ exhibits $U^{\dagger }$ as a cartesian conjugate of $U$ (in the sense of Definition 8.6.1.1).
- $(b)$
The functor $F$ restricts to an equivalence of $\operatorname{\mathcal{E}}^{\dagger }$ with the full subcategory
\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \subseteq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \]
introduced in Construction 8.6.2.2.
Proof.
Let $\lambda = (\lambda _{-}, \lambda _{+}): \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}$ denote the twisted arrow fibration of Example 8.2.0.2. Recall that $(a)$ is equivalent to the following pair of conditions:
- $(a_1)$
For every object $C \in \operatorname{\mathcal{C}}$, the restriction of $T$ to the fiber over the vertex $\{ \operatorname{id}_{C} \} \subseteq \operatorname{Tw}(\operatorname{\mathcal{C}})$ determines an equivalence of $\infty $-categories $T_{C}: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ C\} \rightarrow \{ C \} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$.
- $(a_2)$
Let $(e',e)$ be an edge of the fiber product $\operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$. If $e'$ is a $U^{\dagger }$-cartesian morphism of $\operatorname{\mathcal{E}}^{\dagger }$, then $T(e',e)$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$.
Unwinding the definitions, we see that $F$ factors through $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ if and only if $T$ satisfies the following weaker version of $(a_2)$:
- $(b_0)$
Let $(e',e)$ be an edge of the fiber product $\operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$. If $e'$ is a degenerate edge of $\operatorname{\mathcal{E}}^{\dagger }$, then $T(e',e)$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$.
If this condition is satisfied, then we have a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger } \ar [rr]^{F} \ar [dr]^{ U^{\dagger } } & & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \ar [dl]^{ V } \\ & \operatorname{\mathcal{C}}^{\operatorname{op}}, & } \]
where the vertical maps are cartesian fibrations (Lemma 8.6.2.7). Using Theorem 5.1.6.1, we see that $F$ is an equivalence if and only if it satisfies the following further conditions:
- $(b_1)$
For each object $C \in \operatorname{\mathcal{C}}$, the functor $F$ restricts to an equivalence of $\infty $-categories
\[ F_{C}: \operatorname{\mathcal{E}}^{\dagger }_{C} = \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}}} \{ C\} \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ C\} . \]
- $(b_2)$
The functor $F$ carries $U^{\dagger }$-cartesian morphisms of $\operatorname{\mathcal{E}}^{\dagger }$ to $V$-cartesian morphisms of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$.
Let $C$ be an object of $\operatorname{\mathcal{C}}$. Unwinding the definitions, we can identify the fiber
\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ C\} \]
with the $\infty $-category $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \{ C\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{\mathcal{E}})$. Since $\operatorname{id}_{C}$ is initial when viewed as an object of the $\infty $-category $\{ C\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$ (Proposition 8.1.2.1), Proposition 5.3.1.21 guarantees that the evaluation map
\[ \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \{ C\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}), \operatorname{\mathcal{E}}) \rightarrow \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}} \]
is a trivial Kan fibration. Moreover, the composition of this evaluation map with the functor $F_{C}$ coincides with the functor $T_{C}$ appearing in condition $(a_1)$. It follows that conditions $(a_1)$ and $(b_1)$ are equivalent.
Using the characterization of $V$-cartesian morphisms supplied by Lemmas 8.6.2.6 and 8.6.2.7, we can reformulate $(b_2)$ more concretely as follows:
- $(b'_2)$
Let $(e',e)$ be an edge of the fiber product $\operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$. If $e'$ is a $U^{\dagger }$-cartesian morphism of $\operatorname{\mathcal{E}}^{\dagger }$ and $\lambda _{+}(e)$ is an isomorphism in $\operatorname{\mathcal{C}}$, then $T(e',e)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}$.
To complete the proof, it will suffice to show that the functor $T$ satisfies $(a_2)$ if and only if it satisfies both $(b_0)$ and $(b'_2)$. The implication $(a_2) \Rightarrow (b_0)$ is immediate, and the implication $(a_2) \Rightarrow (b'_2)$ follows from Corollary 5.1.1.8. The reverse implication follows from Proposition 8.6.1.13.
$\square$