Lemma 23.1.12. The following closure properties hold for cocartesian fibrations.
- (1)
-
If \(q\colon E\to D\) and \(p\colon D\to C\) are cocartesian fibrations, then \(pq\colon E\to C\) is a cocartesian fibration, and \(q\) is a cocartesian functor over \(C\).
- (2)
-
Consider a pullback square
If \(p\) is a cocartesian fibration, then so is \(p'\), and a morphism in \(E'\) is \(p'\)-cocartesian if and only if its image under \(F\) is \(p\)-cocartesian.
Proof. For part (1), pick a cocartesian lift along \(p\) of a morphism in \(C\), and then a further cocartesian lift along \(q\). The two defining pullback squares paste to show that the resulting morphism in \(E\) is \(pq\)-cocartesian. This proves that \(pq\) is a cocartesian fibration. By Lemma 23.1.7, every \(pq\)-cocartesian lift is isomorphic to one constructed in this way, so \(q\) carries it to a \(p\)-cocartesian morphism.
For part (2), a \(p\)-cocartesian lift of the image in \(C\) of a morphism in \(C'\) determines a morphism in the pullback \(E'\). The universal property of the pullback identifies its defining cocartesian square with the base change of the corresponding square for \(p\), so this morphism is \(p'\)-cocartesian. Hence \(p'\) is a cocartesian fibration. The same argument proves that every morphism whose image under \(F\) is \(p\)-cocartesian is \(p'\)-cocartesian; the converse follows from uniqueness of cocartesian lifts. □
Generated from the authoritative LaTeX source.