The Stacks project

Proof. Please take a look at the discussion surrounding Categories, Definitions 4.33.1 and 4.33.5 before reading this proof. Let $(a, \beta ) : (U, y) \to (U', y')$ be a morphism of $u^ p\mathcal{S}$. We claim that $(a, \beta )$ is strongly cartesian if and only if $\beta $ is strongly cartesian. First, assume $\beta $ is strongly cartesian. Consider any second morphism $(a_1, \beta _1) : (U_1, y_1) \to (U', y')$ of $u^ p\mathcal{S}$. Then

the second equality as $\beta $ is strongly cartesian. Hence we see that indeed $(a, \beta )$ is strongly cartesian. Conversely, suppose that $(a, \beta )$ is strongly cartesian. Choose a strongly cartesian morphism $\beta ' : y'' \to y'$ in $\mathcal{S}$ with $p(\beta ') = u(a)$. Then bot $(a, \beta ) : (U, y) \to (U, y')$ and $(a, \beta ') : (U, y'') \to (U, y)$ are strongly cartesian and lift $a$. Hence, by the uniqueness of strongly cartesian morphisms (see discussion in Categories, Section 4.33) there exists an isomorphism $\iota : y \to y''$ in $\mathcal{S}_{u(U)}$ such that $\beta = \beta ' \circ \iota $, which implies that $\beta $ is strongly cartesian in $\mathcal{S}$ by Categories, Lemma 4.33.2.

Finally, we have to show that given $(U', y')$ and $U \to U'$ we can find a strongly cartesian morphism $(U, y) \to (U', y')$ in $u^ p\mathcal{S}$ lifting the morphism $U \to U'$. This follows from the above as by assumption we can find a strongly cartesian morphism $y \to y'$ lifting the morphism $u(U) \to u(U')$. $\square$