Lemma 4.33.11. Let $\mathcal{C}$ be a category. Let $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$. If $p : \mathcal{S} \to \mathcal{C}$ is a fibred category and $p$ factors through $p' : \mathcal{S} \to \mathcal{C}/U$ then $p' : \mathcal{S} \to \mathcal{C}/U$ is a fibred category.

Proof. Suppose that $\varphi : x' \to x$ is strongly cartesian with respect to $p$. We claim that $\varphi$ is strongly cartesian with respect to $p'$ also. Set $g = p'(\varphi )$, so that $g : V'/U \to V/U$ for some morphisms $f : V \to U$ and $f' : V' \to U$. Let $z \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$. Set $p'(z) = (W \to U)$. To show that $\varphi$ is strongly cartesian for $p'$ we have to show

$\mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(z, x') \longrightarrow \mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(z, x) \times _{\mathop{\mathrm{Mor}}\nolimits _{\mathcal{C}/U}(W/U, V/U)} \mathop{\mathrm{Mor}}\nolimits _{\mathcal{C}/U}(W/U, V'/U),$

given by $\psi ' \longmapsto (\varphi \circ \psi ', p'(\psi '))$ is bijective. Suppose given an element $(\psi , h)$ of the right hand side, then in particular $g \circ h = p(\psi )$, and by the condition that $\varphi$ is strongly cartesian we get a unique morphism $\psi ' : z \to x'$ with $\psi = \varphi \circ \psi '$ and $p(\psi ') = h$. OK, and now $p'(\psi ') : W/U \to V/U$ is a morphism whose corresponding map $W \to V$ is $h$, hence equal to $h$ as a morphism in $\mathcal{C}/U$. Thus $\psi '$ is a unique morphism $z \to x'$ which maps to the given pair $(\psi , h)$. This proves the claim.

Finally, suppose given $g : V'/U \to V/U$ and $x$ with $p'(x) = V/U$. Since $p : \mathcal{S} \to \mathcal{C}$ is a fibred category we see there exists a strongly cartesian morphism $\varphi : x' \to x$ with $p(\varphi ) = g$. By the same argument as above it follows that $p'(\varphi ) = g : V'/U \to V/U$. And as seen above the morphism $\varphi$ is strongly cartesian. Thus the conditions of Definition 4.33.5 are satisfied and we win. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).