Proof.
According to Categories, Definition 4.27.1 we have to check RMS1, RMS2, RMS3. Condition RMS1 holds as a composition of strongly cartesian morphisms is strongly cartesian, see Categories, Lemma 4.33.2.
To check RMS2 suppose we have a morphism
\[ (a, b, \alpha ) : (U_1, \phi _1 : V_1 \to u(U_1), x_1) \longrightarrow (U, \phi : V \to u(U), x) \]
of $u_{pp}\mathcal{S}$ and a morphism
\[ (c, \text{id}_ V, \gamma ) : (U', \phi ' : V \to u(U'), x') \longrightarrow (U, \phi : V \to u(U), x) \]
with $\gamma $ strongly cartesian from $R$. In this situation set $U'_1 = U_1 \times _ U U'$, and denote $a' : U'_1 \to U'$ and $c' : U'_1 \to U_1$ the projections. As $u(U'_1) = u(U_1) \times _{u(U)} u(U')$ we see that $\phi '_1 = (\phi _1, \phi ') : V_1 \to u(U'_1)$ is a morphism in $\mathcal{D}$. Let $\gamma _1 : x_1' \to x_1$ be a strongly cartesian morphism of $\mathcal{S}$ with $p(\gamma _1) = \phi '_1$ (which exists because $\mathcal{S}$ is a fibred category over $\mathcal{C}$). Then as $\gamma : x' \to x$ is strongly cartesian there exists a unique morphism $\alpha ' : x'_1 \to x'$ with $p(\alpha ') = a'$. At this point we see that
\[ (a', b, \alpha ') : (U_1, \phi _1 : V_1 \to u(U'_1), x'_1) \longrightarrow (U, \phi : V \to u(U'), x') \]
is a morphism and that
\[ (c', \text{id}_{V_1}, \gamma _1) : (U'_1, \phi '_1 : V_1 \to u(U'_1), x'_1) \longrightarrow (U_1, \phi : V_1 \to u(U_1), x_1) \]
is an element of $R$ which form a solution of the existence problem posed by RMS2.
Finally, suppose that
\[ (a, b, \alpha ), (a', b', \alpha ') : (U_1, \phi _1 : V_1 \to u(U_1), x_1) \longrightarrow (U, \phi : V \to u(U), x) \]
are two morphisms of $u_{pp}\mathcal{S}$ and suppose that
\[ (c, \text{id}_ V, \gamma ) : (U, \phi : V \to u(U), x) \longrightarrow (U', \phi : V \to u(U'), x') \]
is an element of $R$ which equalizes the morphisms $(a, b, \alpha )$ and $(a', b', \alpha ')$. This implies in particular that $b = b'$. Let $d : U_2 \to U_1$ be the equalizer of $a, a'$ which exists (see Categories, Lemma 4.18.3). Moreover, $u(d) : u(U_2) \to u(U_1)$ is the equalizer of $u(a), u(a')$ hence (as $b = b'$) there is a morphism $\phi _2 : V_1 \to u(U_2)$ such that $\phi _1 = u(d) \circ \phi _1$. Let $\delta : x_2 \to x_1$ be a strongly cartesian morphism of $\mathcal{S}$ with $p(\delta ) = u(d)$. Now we claim that $\alpha \circ \delta = \alpha ' \circ \delta $. This is true because $\gamma $ is strongly cartesian, $\gamma \circ \alpha \circ \delta = \gamma \circ \alpha ' \circ \delta $, and $p(\alpha \circ \delta ) = p(\alpha ' \circ \delta )$. Hence the arrow
\[ (d, \text{id}_{V_1}, \delta ) : (U_2, \phi _2 : V_1 \to u(U_2), x_2) \longrightarrow (U_1, \phi _1 : V_1 \to u(U_1), x_1) \]
is an element of $R$ and equalizes $(a, b, \alpha )$ and $(a', b', \alpha ')$. Hence $R$ satisfies RMS3 as well.
$\square$
Comments (0)
There are also: