Kerodon

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

Proposition 8.6.3.11. Let $\operatorname{\mathcal{C}}$ be a simplicial set, 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 morphism $T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ for which the diagram

\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [r]^-{T} \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{ U } \\ \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [r] & \operatorname{\mathcal{C}}} \]

is commutative. The following conditions are equivalent:

$(a)$

The morphism $T$ exhibits $U^{\dagger }$ as a cartesian conjugate of $U$, in the sense of Definition 8.6.1.1.

$(b)$

The comparison map $\Psi $ of Construction 8.6.3.9 factors through the simplicial set $\operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ of Notation 8.6.3.1, and the map $\operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ is an equivalence of cartesian fibrations over $\operatorname{\mathcal{C}}$.

Proof. Using Proposition 5.1.7.15, we see that $(b)$ is equivalent to the following three conditions:

$(b_0)$

The map $\Psi $ factors through the simplicial subset $\operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \subseteq \operatorname{Cospan}(\operatorname{\mathcal{E}}) \times _{\operatorname{Cospan}(\operatorname{\mathcal{C}})} \operatorname{\mathcal{C}}^{\operatorname{op}}$.

$(b_1)$

Let $V: \operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be the cartesian fibration of Lemma 8.6.3.8. Then $\Psi $ carries $U^{\dagger }$-cartesian edges of $\operatorname{\mathcal{E}}^{\dagger }$ to $V$-cartesian edges of $\operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$.

$(b_2)$

For each vertex $C \in \operatorname{\mathcal{C}}$, the morphism $\Psi $ restricts to an equivalence of $\infty $-categories

\[ \Psi _{C}: \operatorname{\mathcal{E}}^{\dagger }_{C} \rightarrow \operatorname{Cospan}^{\dagger }( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \{ C\} = \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}( \operatorname{\mathcal{E}}_{C} ). \]

For every edge $e: D \rightarrow C$ of $\operatorname{\mathcal{C}}$, let $e_{L}: \operatorname{id}_{D} \rightarrow e$ and $e_{R}: \operatorname{id}_{C} \rightarrow e$ denote the edges of $\operatorname{Tw}(\operatorname{\mathcal{C}})$ described in Example 8.1.3.6. Using Remark 8.6.3.10, we can rewrite condition $(b_0)$ as follows:

$(b'_0)$

Let $Y$ be a vertex of $\operatorname{\mathcal{E}}^{\dagger }$ having image $D = U^{\dagger }(Y)$ in $\operatorname{\mathcal{C}}$, and let $e: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$. Then $T( \operatorname{id}_{Y}, e_{L} ): T(Y, \operatorname{id}_{D} ) \rightarrow T( Y, e )$ is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$.

Similarly, by combining Remark 8.6.3.10 with the characterization of $V$-cartesian edges supplied by Lemma 8.6.3.8, we can rewrite condition $(b_1)$ as follows:

$(b'_1)$

Let $f: X \rightarrow Y$ be a $U^{\dagger }$-cartesian edge of $\operatorname{\mathcal{E}}^{\dagger }$, and let us identify $U^{\dagger }(f)$ with an edge $e: D \rightarrow C$ of $\operatorname{\mathcal{C}}$. Then $T(f, e_{R} ): T(X, \operatorname{id}_{C}) \rightarrow T(Y,e)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$.

Unwinding the definitions, we observe that for each vertex $C \in \operatorname{\mathcal{C}}$, the functor $\Psi _{C}$ factors as a composition

\[ \operatorname{\mathcal{E}}^{\dagger }_{C} \xrightarrow { T_{C} } \operatorname{\mathcal{E}}_{C} \hookrightarrow \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}( \operatorname{\mathcal{E}}_{C} ) \simeq \operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ C\} , \]

where the second map is the equivalence of Proposition 8.1.7.6. We can therefore rewrite $(b_2)$ as follows:

$(b'_2)$

For each vertex $C \in \operatorname{\mathcal{C}}$, the morphism $T$ restricts to an equivalence of $\infty $-categories $T_{C}: \operatorname{\mathcal{E}}^{\dagger }_{C} \rightarrow \operatorname{\mathcal{E}}_{C}$.

The equivalence of $(a)$ and $(b)$ now follows from Proposition 8.6.1.13. $\square$