Theorem 15.1.7 (Barwick (2017), [Haugseng et al. (2023), Theorem 3.1]). Let \(p\colon (E,E_L,E_R) \to (C,C_L,C_R)\) be a morphism of adequate triples, and consider a span \[ X \xleftarrow {\phi } U \xrightarrow {\psi } Y, \] with \(\phi \in E_L\) and \(\psi \in E_R\). Then this morphism is cocartesian with respect to \(\Span (p)\colon \Span _{L,R}(E) \to \Span _{L,R}(C)\) whenever the following conditions are satisfied:
- (1)
-
The morphism \(\phi \) is \(p\)-cartesian and the morphism \(\psi \) is \(p\)-cocartesian;
- (2)
-
(Left cancellation for \(E_L\)) Given a commutative triangle
such that \(p(\xi ) \in C_L\) and \(\phi \xi \in E_L\), we have \(\xi \in E_L\);
- (3)
-
(Right cancellation for \(E_R\)) Given a commutative triangle
such that \(p(\xi ) \in C_R\) and \(\xi \psi \in E_R\), we have \(\xi \in E_R\);
- (4)
-
(Enough \(p\)-cocartesian lifts) For any pullback square in \(C\) of the form
with \(l \in C_L\), and for any \(W \in E_{K}\), the morphism \(g\) admits a \(p\)-cocartesian lift \(\psi '\colon W \to V\) which lies in \(E_R\) and also satisfies the condition from (3);
- (5)
-
(Beck–Chevalley) Consider a commutative square in \(E\) of the form
such that its image in \(C\) is a pullback square, \(\xi ' \in E_L\), \(\psi ' \in E_R\), and \(p(\xi ) \in C_L\). Then \(\psi '\) is \(p\)-cocartesian if and only if \(\xi \in E_L\) and the square is a pullback square.
Proof. We consider any other span \(X \leftarrow W \to Z\) in \(E\). We have to show that every prescribed filling of the image in \(C\) of the following dashed diagram admits a unique lift to a filling in \(E\):
Here all left-pointing maps are in \(E_L\) and all right-pointing maps are in \(E_R\). By the description of the hom animae of a span category from Lemma 13.1.13, the anima of such fillings is precisely the fiber of the comparison map \[ \Hom _{\Span _{L,R}(E)}(Y,Z) \longrightarrow \Hom _{\Span _{L,R}(E)}(X,Z) \times _{\Hom _{\Span _{L,R}(C)}(pX,pZ)} \Hom _{\Span _{L,R}(C)}(pY,pZ) \] over the given point, so that showing all these fibers to be contractible is exactly showing that our span is \(\Span (p)\)-cocartesian. We produce the filling in three steps, each of which is unique up to a contractible choice.
- (i)
-
Since \(\phi \) is \(p\)-cartesian, there exists a unique lift \(W \to U\) making the left triangle commute, which lies in \(E_L\) by condition (2).
- (ii)
-
We claim that this lift \(W \to U\) may uniquely be written as the pullback along \(\psi \) of some morphism \(V \to Y\) in \(E_L\) compatible with the given pullback square in \(C\); more precisely, we claim that the following commutative square is a pullback square:
Here the superscript \((-)^{L}\) means that we take the full subcategories spanned by the morphisms in \(E_L\) and \(C_L\), respectively.
- (a)
-
For essential surjectivity of \((E_{/Y})^L \to (E_{/U})^L \times _{(C_{/pU})^L} (C_{/pY})^L\), we consider a morphism \(\xi '\colon W \to U\) in \(E_L\) and assume we are given a pullback square in \(C\) of the form
with \(l \in C_L\). By assumption (4) we can find a \(p\)-cocartesian lift \(\psi '\colon W \to V\) of \(g\) which lies in \(E_R\) and satisfies condition (3). The composite \(\psi \circ \xi '\colon W \to Y\) then factors through a map \(\xi \colon V \to Y\), giving a commutative square in \(E\) of the form considered in (5). By assumption (5), the map \(\xi \) then lies in \(E_L\) and the resulting square is a pullback square. As \(\xi \) lifts \(l\), this shows that the pair \((\xi ',l)\) lies in the essential image, as desired.
- (b)
-
For full faithfulness, consider two objects \(\xi _1\colon V_1 \to Y\) and \(\xi _2\colon V_2 \to Y\) of \((E_{/Y})^L\). We must show that the commutative square
is a pullback square. By the universal property of pullbacks, the right vertical map is isomorphic to the map \[ p\colon \Hom _{E_{/Y}}(U \times _Y V_1, V_2) \to \Hom _{C_{/pY}}(pU \times _{pY} pV_1, pV_2), \] hence the claim follows from the fact that the projection map \(U \times _Y V_1 \to V_1\) is \(p\)-cocartesian: this is the implication from right to left in assumption (5), applied to the pullback square of \(\xi _1\) along \(\psi \), whose remaining two sides lie in \(E_L\) and \(E_R\) by adequacy. This morphism remains cocartesian after passing to the slice over \(Y\), since its cocartesian universal property is unchanged when the target is fixed.
- (iii)
-
Finally, given a \(p\)-cocartesian morphism \(W \to V\), the given map \(W \to Z\) uniquely factors through a map \(V \to Z\), which lies in \(E_R\) by condition (3). □
Generated from the authoritative LaTeX source.