Kerodon

Proof. Combine Proposition 8.6.6.1 with Remark 8.6.4.3. $\square$

Proof. Combine Proposition 8.6.6.1 with Corollary 8.6.5.2. $\square$

Proof. Combine Propositions 8.6.6.1 and 8.6.3.5. $\square$

Proof. We will show that $(2)$ implies $(1)$; the reverse implication follows from Proposition 8.6.2.10. Using Corollary 8.6.6.3, we can choose a cocartesian fibration $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ and a commutative diagram

which exhibits $U^{\dagger }$ as a cartesian conjugate of $U'$. Assume that condition $(2)$ is satisfied, so that we have a commutative diagram

where the horizontal maps are equivalences of $\infty $-categories and the vertical maps are isofibrations (Corollary 4.4.5.6). Applying Corollary 4.5.2.32, we deduce that the map

is fully faithful, and that its essential image consists of those functors $\operatorname{\mathcal{E}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}'$ which carry each morphism of $W$ to an isomorphism in $\operatorname{\mathcal{E}}'$. We may therefore assume without loss of generality that $T' = F \circ T$ for some functor $F \in \operatorname{Fun}_{/ \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}')$. Proposition 8.6.2.10 implies that $T'$ exhibits $\operatorname{\mathcal{E}}'$ as a localization of $\operatorname{\mathcal{E}}^{\dagger } \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$ with respect to $W$. It follows that $F$ is an equivalence of $\infty $-categories (Remark 6.3.1.19), so that $T$ also exhibits $U^{\dagger }$ as a cartesian conjugate of $U$. $\square$

Proof. We first prove $(a)$. Fix an edge $e: C_0 \rightarrow C_1$ of $\operatorname{\mathcal{C}}$, let $\operatorname{\mathcal{E}}_{0}$ denote the fiber $\{ C_0 \} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, and define $\operatorname{\mathcal{E}}_{1}$ similarly. Fix an object $Y \in \operatorname{\mathcal{E}}_0$, so that we can identify the pair $(Y,e)$ with a vertex of the fiber product $\operatorname{\mathcal{E}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$. Then $T(Y,e)$ can be regarded as a functor $F: \operatorname{\mathcal{E}}_{1} \rightarrow \operatorname{\mathcal{S}}^{< \kappa }$, and we wish to show that $F$ is corepresentable. Replacing $U$ by the projection map $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^1$, we can reduce to the special case where $\operatorname{\mathcal{C}}= \Delta ^1$ is the standard $1$-simplex (with $C_0 = 0$ and $C_1 = 1$). Our assumption that $U$ is a cocartesian fibration guarantees that there exists a $U$-cocartesian morphism $f: Y \rightarrow X$ with $X \in \operatorname{\mathcal{E}}_1$. Let $\mathscr {H}: \operatorname{\mathcal{E}}^{\operatorname{op}} \times \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a $\operatorname{Hom}$-functor for $\operatorname{\mathcal{E}}$. Using Example 8.6.6.11, we can identify $F$ with the functor

so that $f$ can be identified with a vertex of $\eta \in F(X)$. Since $f$ is $U$-cocartesian, the vertex $\eta $ exhibits $F$ as corepresented by the object $X$ (see Lemma 8.6.5.14).

We now prove $(b)$. For each vertex $C \in \operatorname{\mathcal{C}}$, the restriction of $T$ to the fiber $\operatorname{\mathcal{E}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ \operatorname{id}_{C} \} $ determines a functor $T_{C}: \operatorname{\mathcal{E}}^{\operatorname{op}}_{C} \rightarrow \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{S}}^{< \kappa } )$ which is a contravariant Yoneda embedding for the $\infty $-category $\operatorname{\mathcal{E}}_{C}$ (Remark 8.6.6.14), and is therefore an equivalence of $\infty $-categories (Theorem 8.3.3.13). We will complete the proof by showing that $T$ satisfies conditions $(2')$ and $(2'')$ of Proposition 8.6.1.13. Both of these conditions make an assertion about an arbitrary edge $e: C_0 \rightarrow C_1$ of the simplicial set $\operatorname{\mathcal{C}}$; let us denote these assertions by $(2'_ e)$ and $(2''_ e)$, respectively. To verify them, we can replace $U$ by the projection map $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^1$ as above, and thereby reduce to the special case where $\operatorname{\mathcal{C}}= \Delta ^1$ is the standard $1$-simplex and $e$ is the nondegenerate edge of $\operatorname{\mathcal{C}}$. Let $\mathscr {H}: \operatorname{\mathcal{E}}^{\operatorname{op}} \times \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a $\operatorname{Hom}$-functor for $\operatorname{\mathcal{E}}$. Using Example 8.6.6.11 again and Variant 8.6.5.11, we can formulate the hypotheses of Proposition 8.6.1.13 more concretely as follows:

$(2'_ e)$

For every object $Y \in \operatorname{\mathcal{E}}_0$, the functor $\mathscr {H}(Y, -): \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ is left Kan extended from $\operatorname{\mathcal{E}}_0$.

$(2''_{e})$

For every object $Y \in \operatorname{\mathcal{E}}_0$ and every $U$-cocartesian morphism $f: Y \rightarrow X$ with $X \in \operatorname{\mathcal{E}}_1$, the induced natural transformation $\mathscr {H}(X, -) \rightarrow \mathscr {H}(Y,-)$ is an isomorphism when restricted to the subcategory $\operatorname{\mathcal{E}}_1$. In other words, for every object $W \in \operatorname{\mathcal{E}}_1$, precomposition with $f$ induces a homotopy equivalence $\mathscr {H}(X,W) \rightarrow \mathscr {H}(Y,W)$.

Assertion $(2'_ e)$ now follows from Lemma 8.6.5.13, and assertion $(2''_{e})$ from Corollary 5.1.2.3. $\square$

Proof of Proposition 8.6.6.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U^{\vee }: \operatorname{\mathcal{E}}^{\vee } \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets. Fix an uncountable cardinal $\kappa $ such that $U$ and $U^{\vee }$ are locally $\kappa $-small. If $U$ is a cocartesian dual of $U^{\vee }$, then Proposition 8.6.5.18 guarantees that $U^{\vee }$ is equivalent to the cocartesian fibration $\pi ^{\operatorname{corep}}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \rightarrow \operatorname{\mathcal{C}}$. Combining this observation with Theorem 8.6.6.15, we conclude that $U^{\operatorname{op}}$ is a cartesian conjugate of $U^{\vee }$.

We now prove the converse. Assume that $U^{\operatorname{op}}$ is a cartesian conjugate of $U^{\vee }$; we wish to show that $U$ is a cartesian dual of $U^{\vee }$. Applying Theorem 8.6.5.1, we see that $U^{\vee }$ admits a cocartesian dual $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$. The first part of the proof shows that the opposite fibration $U'^{\operatorname{op}}: \operatorname{\mathcal{E}}'^{\operatorname{op}} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is a cartesian conjugate of $U^{\vee }$, and is therefore equivalent to the cartesian fibration $U^{\operatorname{op}}$ (Corollary 8.6.3.14). It follows that the cocartesian fibrations $U$ and $U'$ are also equivalent, so that $U$ is also a cocartesian dual of $U^{\vee }$. $\square$