# Kerodon

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

Proposition 8.6.6.6. 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 : \operatorname{\mathcal{E}}^{\dagger , \operatorname{op}} \rightarrow \operatorname{Cospan}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ of Construction 8.6.6.4 factors through the simplicial subset $\operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ of Notation 8.6.5.1. Moreover, $\Psi$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$.

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

$(b_0)$

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

$(b_1)$

Let $U^{\vee }: \operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the cocartesian fibration of Lemma 8.6.5.10. Then $\Psi$ carries $U^{\dagger }$-cartesian edges of $\operatorname{\mathcal{E}}^{\dagger }$ to $U^{\vee }$-cocartesian edges of $\operatorname{Cospan}^{\operatorname{CCart}}(\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})^{\operatorname{op}} \rightarrow \{ C\} \times _{ \operatorname{\mathcal{C}}} \operatorname{Cospan}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) = \operatorname{Cospan}^{ \mathrm{iso}, \mathrm{all}}( \operatorname{\mathcal{E}}_{C} ).$

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

$(b'_0)$

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

Similarly, by combining Remark 8.6.6.5 with the characterization of $U^{\vee }$-cartesian edges supplied by Lemma 8.6.5.10, we can rewrite condition $(b_1)$ as follows:

$(b'_1)$

Let $f: Y \rightarrow X$ be a $U^{\dagger }$-cartesian edge of $\operatorname{\mathcal{E}}^{\dagger }$, and let us identify $U^{\dagger }(f)$ with an edge $e: C \rightarrow D$ of $\operatorname{\mathcal{C}}$. Then $T(f, e_{R} ): T(Y, \operatorname{id}_{D}) \rightarrow T(X,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})^{\operatorname{op}} \xrightarrow { T_{C}^{\operatorname{op}} } \operatorname{\mathcal{E}}^{\operatorname{op}}_{C} \hookrightarrow \operatorname{Cospan}^{ \mathrm{iso}, \mathrm{all}}( \operatorname{\mathcal{E}}_{C} ),$

where the second map is the equivalence of Variant 8.1.7.14. 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$