Kerodon

Proof. Combine Theorem 8.6.5.6 with Example 8.6.5.5. $\square$

Proof. Let $L_0$ be the collection of all morphisms in $\operatorname{\mathcal{C}}$, and let $R_0$ be the collection of all morphisms of $\operatorname{\mathcal{C}}$. Then $L_0$ and $R_0$ are pushout-compatible, in the sense of Definition 8.1.6.5 (Example 8.1.6.6). Moreover, $U$ is a Beck-Chevalley fibration relative to $(R_0, L_0)$ (Example 8.1.10.8). Since $\operatorname{Cospan}^{L_0, R_0}(\operatorname{\mathcal{C}}) = \operatorname{Cospan}^{\mathrm{iso}, \mathrm{all}}(\operatorname{\mathcal{C}})$ is an $\infty $-category, the desired result follows from (the duals of) Theorem 8.1.10.9 and Remark 8.1.10.11. $\square$

Proof. Using Proposition 5.1.4.7 and Remark 8.6.5.4, we can reduce to the case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex. In particular, $\operatorname{\mathcal{C}}$ is an $\infty $-category. In this case, the desired result follows by combining Remark 8.6.5.9 with Lemma 8.6.5.8. $\square$

Proof of Theorem 8.6.5.6 from Proposition 8.6.5.12. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $U^{\vee }: \operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the projection map; we wish to show that $U^{\vee }$ is a cocartesian dual of $U$. Using Corollary 5.7.7.3, we can choose a pullback diagram

where $U'$ is a cocartesian fibration of $\infty $-categories. Using Remarks 8.6.3.4 and 8.6.5.4, we can replace $U$ by $U'$ and thereby reduce to the case where $\operatorname{\mathcal{C}}$ is an $\infty $-category. In this case, we have commutative diagrams

where the vertical maps are cocartesian fibrations, the diagram on the left is a pullback square, and the diagram on the right is a categorial pullback square (the horizontal maps are equivalences of $\infty $-categories by virtue of Proposition 8.1.7.6). Using Remark 8.6.3.4 again, we are reduced to showing that $V_{-}$ is a cocartesian dual of $V_{+}$, which follows from Proposition 8.6.5.12. $\square$

Proof. Let $\pi : \operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}$ denote the functor given by projection onto the second factor. Let $L'$ denote the collection of all $\pi $-cocartesian morphisms of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$: that is, morphisms $(u,v)$ where $u$ is a $U$-cocartesian morphism in $\operatorname{\mathcal{E}}$. Let $R'$ denote the collection of all morphisms $(u,v)$ of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ where $v$ is an isomorphism in $\operatorname{\mathcal{E}}$. It follows from Proposition 8.1.9.10 (and Example 8.1.6.6) that the pair $(L',R')$ is pushout-compatible, in the sense of Definition 8.1.6.5. Moreover, we have a canonical isomorphism of simplicial sets

Using Lemma 8.6.5.8, we see that $\pi $ induces a cocartesian fibration $\operatorname{Cospan}^{L',R'}(\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}})$, where the target is an $\infty $-category (Proposition 8.1.7.5). It follows that the simplicial set $\operatorname{Cospan}^{L',R'}(\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}})$ is also an $\infty $-category.

Let $\operatorname{ev}_0, \operatorname{ev}_{1}: \operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{E}}$ denote functors given by evaluation at $0,1 \in \Delta ^1$, so that $\operatorname{ev}_0$ and $\operatorname{ev}_1$ determine a functor

By construction we have $\widetilde{L} = \operatorname{ev}^{-1}( L' )$ and $\widetilde{R} = \operatorname{ev}^{-1}( R' )$. Note that $\operatorname{ev}$ is a pullback of the map $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}) = \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Moreover, we can identify $V$ with the map

induced by $\operatorname{ev}$. By virtue of Example 8.1.10.13, to show that $V$ is a left fibration, it will suffice to verify the following:

$(0)$

Every element of $\widetilde{L}$ is $\operatorname{ev}$-cocartesian, and every element of $\widetilde{R}$ is $\operatorname{ev}$-cartesian. This follows from Lemma 5.3.7.1.

$(1)$

Fix an object $C \in \operatorname{\mathcal{C}}$ and a morphism $f: X \rightarrow Y$ in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, which we identify with an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$. Let $(u,v): (X',Y') \rightarrow (X,Y)$ be a morphism of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ which belongs to $R'$ (so that $v$ is an isomorphism in $\operatorname{\mathcal{E}}$). Then we can write $(u,v) = \operatorname{ev}(w)$ for some morphism $w: f' \rightarrow f$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ (the morphism $w$ then belongs to $\widetilde{R}$ and is therefore automatically $\operatorname{ev}$-cartesian). To prove this, we note that $U(u) = U(v)$ determines an edge $\Delta ^1 \rightarrow \operatorname{\mathcal{C}}$. Replacing $\operatorname{\mathcal{E}}$ by the fiber product $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, we can reduce to the situation where $\operatorname{\mathcal{C}}= \Delta ^1$ is a standard simplex. In this case, we are reduced to the problem of constructing a diagram $\Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{E}}$ whose boundary is indicated in the simplex

\[ \xymatrix@R =50pt@C=50pt{ X' \ar@ {-->}[r]^{f'} \ar [d]^{u} & Y' \ar [d]^{v} \\ X \ar [r]^-{f} & Y, } \]

which is possible by virtue of our assumption that $v$ is an isomorphism.

$(2)$

Fix an object $C \in \operatorname{\mathcal{C}}$ and a morphism $f: X \rightarrow Y$ as above, and let $(u,v): (X,Y) \rightarrow (X',Y')$ be a morphism of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ which belongs to $L'$ (so that $u$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$). Then we can write $(u,v) = \operatorname{ev}(w)$, for some morphism $w: f \rightarrow f'$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ (the morphism $w$ then belongs to $\widetilde{L}$ and is therefore automatically $\operatorname{ev}$-cocartesian). This follows from Proposition 5.3.7.2 (or by a direct argument similar to the proof of $(1)$).

Proof of Proposition 8.6.5.12. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories, and let

be the left fibration of Lemma 8.6.5.14. We wish to show that the left fibraiton $V$ exhibits $V_{-}: \operatorname{Cospan}^{L,R}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$ as a cocartesian dual of $V_{+}: \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$. For each object $C \in \operatorname{\mathcal{C}}$, let $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ denote the corresponding fiber of $U$. Then we have a canonical isomorphism

where $\widetilde{L}_{C}$ denotes the collection of all morphisms of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}_{C} )$ for which the image in $\operatorname{Fun}( \{ 0\} , \operatorname{\mathcal{E}}_{C} )$ is an isomorphism, and $\widetilde{R}_{C}$ denotes the collection of morphisms $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}_{C} )$ for which the image in $\operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{E}}_{C} )$ is an isomorphism. The left fibration $V$ then restricts to a coupling of $\infty $-categories

which is balanced by virtue of Proposition 8.2.6.9. Moreover, if $f$ is an object of the $\infty $-category $\operatorname{Cospan}^{ \widetilde{L}, \widetilde{R} }( \operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) )$ satisfying $V(f) = C$, then $f$ is universal (with respect to the coupling $V_{C}$) if and only if it is an isomorphism when regarded as a morphism in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$ (Corollary 8.2.6.14).

Let $u: f \rightarrow g$ be a morphism in the $\infty $-category $\operatorname{Cospan}^{ \widetilde{L}, \widetilde{R} }( \operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) )$, having image $\overline{u}: C \rightarrow D$ in the $\infty $-category $\operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$. Assume that the image of $u$ in $\operatorname{Cospan}^{L,R}(\operatorname{\mathcal{E}})$ is $V_{-}$-cocartesian and that the image of $u$ in $\operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}})$ is $V_{+}$-cocartesian. To complete the proof, we must show that if $f$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, then $g$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{D}$. To prove this, let us identify $u$ with a commutative diagram

in the $\infty $-category $\operatorname{\mathcal{E}}$, where $s_{-}$ is $U$-cocartesian and $t_{+}$ is an isomorphism. Since the image of $u$ in $\operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso} }(\operatorname{\mathcal{E}})$ is $V_{+}$-cocartesian, the morphism $s_{+}$ is $U$-cocartesian. Applying Corollary 5.1.2.4, we deduce that the morphism $h$ is $U$-cocartesian. Since the image of $u$ in $\operatorname{Cospan}^{ L,R}(\operatorname{\mathcal{E}})$ is $V_{-}$-cocartesian, the morphism $t_{-}$ is an isomorphism. Applying Corollary 5.1.2.5, we deduce that $g$ is $U$-cocartesian when regarded as a morphism of $\operatorname{\mathcal{E}}$, and is therefore an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{D}$ (Example 5.1.3.6). $\square$