The Stacks project

Proof. Let us make a choice of pullbacks (see Definition 4.33.6). By Lemma 4.33.7 we get pullback functors $f^*$ for every morphism $f$ of $\mathcal{C}$.

We construct a new category $\mathcal{S}'$ as follows. The objects of $\mathcal{S}'$ are pairs $(x, f)$ consisting of a morphism $f : V \to U$ of $\mathcal{C}$ and an object $x$ of $\mathcal{S}$ over $U$, i.e., $x\in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_ U)$. The functor $p' : \mathcal{S}' \to \mathcal{C}$ will map the pair $(x, f)$ to the source of the morphism $f$, in other words $p'(x, f : V\to U) = V$. A morphism $\varphi : (x_1, f_1: V_1 \to U_1) \to (x_2, f_2 : V_2 \to U_2)$ is given by a pair $(\varphi , g)$ consisting of a morphism $g : V_1 \to V_2$ and a morphism $\varphi : f_1^\ast x_1 \to f_2^\ast x_2$ with $p(\varphi ) = g$. It is no problem to define the composition law: $(\varphi , g) \circ (\psi , h) = (\varphi \circ \psi , g\circ h)$ for any pair of composable morphisms. There is a natural functor $\mathcal{S} \to \mathcal{S}'$ which simply maps $x$ over $U$ to the pair $(x, \text{id}_ U)$.

At this point we need to check that $p'$ makes $\mathcal{S}'$ into a fibred category over $\mathcal{C}$, and we need to check that $\mathcal{S} \to \mathcal{S}'$ is an equivalence of categories over $\mathcal{C}$ which maps strongly cartesian morphisms to strongly cartesian morphisms. We omit the verifications.

Finally, we can define pullback functors on $\mathcal{S}'$ by setting $g^\ast (x, f) = (x, f \circ g)$ on objects if $g : V' \to V$ and $f : V \to U$. On morphisms $(\varphi , \text{id}_ V) : (x_1, f_1) \to (x_2, f_2)$ between morphisms in $\mathcal{S}'_ V$ we set $g^\ast (\varphi , \text{id}_ V) = (g^\ast \varphi , \text{id}_{V'})$ where we use the unique identifications $g^\ast f_ i^\ast x_ i = (f_ i \circ g)^\ast x_ i$ from Lemma 4.33.7 to think of $g^\ast \varphi$ as a morphism from $(f_1 \circ g)^\ast x_1$ to $(f_2 \circ g)^\ast x_2$. Clearly, these pullback functors $g^\ast$ have the property that $g_1^\ast \circ g_2^\ast = (g_2\circ g_1)^\ast$, in other words $\mathcal{S}'$ is split as desired. $\square$