The Stacks project

Proof. Denote $p : \mathcal{X} \to \mathcal{C}$ and $q : \mathcal{Y} \to \mathcal{C}$ the structure functors. We construct $\mathcal{X}'$ explicitly as follows. An object of $\mathcal{X}'$ is a quadruple $(U, x, y, f)$ where $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{X}_ U)$, $y \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{Y}_ U)$ and $f : y \to F(x)$ is a morphism in $\mathcal{Y}_ U$. A morphism $(a, b) : (U, x, y, f) \to (U', x', y', f')$ is given by $a : x \to x'$ and $b : y \to y'$ with $p(a) = q(b) : U \to U'$ and such that $f' \circ b = F(a) \circ f$.

Let us make a choice of pullbacks for both $p$ and $q$ and let us use the same notation to indicate them. Let $(U, x, y, f)$ be an object and let $h : V \to U$ be a morphism. Consider the morphism $c : (V, h^*x, h^*y, h^*f) \to (U, x, y, f)$ coming from the given strongly cartesian maps $h^*x \to x$ and $h^*y \to y$. We claim $c$ is strongly cartesian in $\mathcal{X}'$ over $\mathcal{C}$. Namely, suppose we are given an object $(W, x', y', f')$ of $\mathcal{X}'$, a morphism $(a, b) : (W, x', y', f') \to (U, x, y, f)$ lying over $W \to U$, and a factorization $W \to V \to U$ of $W \to U$ through $h$. As $h^*x \to x$ and $h^*y \to y$ are strongly cartesian we obtain morphisms $a' : x' \to h^*x$ and $b' : y' \to h^*y$ lying over the given morphism $W \to V$. Consider the diagram

The outer rectangle and the right square commute. Since $F$ is a $1$-morphism of fibred categories the morphism $F(h^*x) \to F(x)$ is strongly cartesian. Hence the left square commutes by the universal property of strongly cartesian morphisms. This proves that $\mathcal{X}'$ is fibred over $\mathcal{C}$.

The functor $u : \mathcal{X} \to \mathcal{X}'$ is given by $x \mapsto (p(x), x, F(x), \text{id})$. This is fully faithful. The functor $\mathcal{X}' \to \mathcal{Y}$ is given by $(U, x, y, f) \mapsto y$. The functor $w : \mathcal{X}' \to \mathcal{X}$ is given by $(U, x, y, f) \mapsto x$. Each of these functors is a $1$-morphism of fibred categories over $\mathcal{C}$ by our description of strongly cartesian morphisms of $\mathcal{X}'$ over $\mathcal{C}$. Adjointness of $w$ and $u$ means that

which follows immediately from the definitions.

Finally, we have to show that $\mathcal{X}' \to \mathcal{Y}$ is a fibred category. Let $c : y' \to y$ be a morphism in $\mathcal{Y}$ and let $(U, x, y, f)$ be an object of $\mathcal{X}'$ lying over $y$. Set $V = q(y')$ and let $h = q(c) : V \to U$. Let $a : h^*x \to x$ and $b : h^*y \to y$ be the strongly cartesian morphisms covering $h$. Since $F$ is a $1$-morphism of fibred categories we may identify $h^*F(x) = F(h^*x)$ with strongly cartesian morphism $F(a) : F(h^*x) \to F(x)$. By the universal property of $b : h^*y \to y$ there is a morphism $c' : y' \to h^*y$ in $\mathcal{Y}_ V$ such that $c = b \circ c'$. We claim that

is strongly cartesian in $\mathcal{X}'$ over $\mathcal{Y}$. To see this let $(W, x_1, y_1, f_1)$ be an object of $\mathcal{X}'$, let $(a_1, b_1) : (W, x_1, y_1, f_1) \to (U, x, y, f)$ be a morphism and let $b_1 = c \circ b_1'$ for some morphism $b_1' : y_1 \to y'$. Then

(where $a_1' : x_1 \to h^*x$ is the unique morphism lying over the given morphism $q(b_1') : W \to V$ such that $a_1 = a \circ a_1'$) is the desired morphism. $\square$