Proposition 15.2.8. Let \(C\) be an \(\infty \)-category. Then the following conditions are equivalent:
- (1)
-
The \(\infty \)-category \(C\) admits finite coproducts;
- (2)
-
The cartesian fibration \(q\colon \Fin (C) \to \Fin \) is a cocartesian fibration;
- (3)
-
The functor \(p_C^{\amalg }=\Span (q)\colon C^{\amalg } \to \Span (\Fin )\) is a cocartesian fibration.
If these conditions hold, \(p_C^{\amalg }\) is the cocartesian unstraightening of the unfurling \((C,\amalg )\) from Proposition 15.2.1.
Proof. If \(C\) admits finite coproducts, we showed above that \(q\colon \Fin (C) \to \Fin \) is a Beck–Chevalley fibration. The construction in Theorem 15.1.3 identifies the cocartesian unstraightening of the unfurling from Proposition 15.2.1 with \(\Span (q)\). This proves that (1) implies (3), as well as the final assertion.
We next show that (3) implies (2). Recall from the dual of Lemma 23.1.15 that every \(q\)-cartesian morphism in \(\Fin (C)\) whose image in \(\Fin \) is an isomorphism is itself an isomorphism. Consequently, the square
is a pullback square. Since cocartesian fibrations are closed under pullback, (3) implies (2).
Finally, suppose that \(q\) is a cocartesian fibration. By Lemma 23.1.20, its cocartesian transport \(f_!\colon C^I \to C^J\) along a map \(f\colon I \to J\) is left adjoint to the cartesian transport \(f^*\colon C^J \to C^I\). For the map \(\emptyset \to \lra {1}\) this produces an initial object of \(C\), while for the fold map \(\lra {2} \to \lra {1}\) it produces binary coproducts. Thus \(C\) admits finite coproducts, proving that (2) implies (1). □
Generated from the authoritative LaTeX source.