Adequate triple from cartesian morphisms

Proof. Both classes are wide subcategories of \(E\): this is clear for \(E_R = p^{-1}(C_R)\), while \(E_L^{p\dcart }\) contains all identities and is closed under composition since \(C_L\) is and since composites of \(p\)-cartesian morphisms are again \(p\)-cartesian.

We next construct the pullback in \(E\) of a morphism \(l\in E_L^{p\dcart }\) along some \(r \in E_R\). Since \(pl \in C_L\) and \(pr \in C_R\), we may form the pullback

in \(C\). By assumption on \(p\), there exists a \(p\)-cartesian lift \(l'\colon X' \to Y'\) of the morphism \(pX \times _{pY} pY' \to pY'\). The composite \(rl'\colon X' \to Y\) then uniquely factorizes through some \(r'\colon X' \to X\) lifting the projection \(pX \times _{pY} pY' \to pX\), using that \(l\) is \(p\)-cartesian. All in all, we have lifted the pullback square in \(C\) to a commutative square in \(E\) of the form

Since \(l\) and \(l'\) are \(p\)-cartesian, it follows from Lemma 15.1.8 that this square is a pullback square in \(E\), showing that the required pullbacks exist. Moreover, in this square we have \(l' \in E_L^{p\dcart }\) and \(r' \in E_R\), so both classes are closed under the relevant base changes. This shows part (1).

For part (2), consider a pullback square in \(E\) of the form (15.1). We need to show that applying \(p\) to this square gives a pullback square in \(C\). Proceeding as before, we may always form the pullback of \(pl\) and \(pr\) in \(C\) and lift this to a pullback square in \(E\). But by uniqueness of pullback squares of \(l\) and \(r\), this new square must then agree with the given one. In particular their images in \(C\) agree, hence this image is a pullback square. □