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 : F(x) \to y$ is an isomorphism 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)$ and such that $f' \circ F(a) = b \circ f$. In other words $\mathcal{X}' = \mathcal{X} \times _{F, \mathcal{Y}, \text{id}} \mathcal{Y}$ with the construction of the $2$-fibre product from Lemma 4.32.3. By Lemma 4.35.7 we see that $\mathcal{X}'$ is a category fibred in groupoids over $\mathcal{C}$ and that $\mathcal{X}' \to \mathcal{Y}$ is a morphism of categories over $\mathcal{C}$. As functor $\mathcal{X} \to \mathcal{X}'$ we take $x \mapsto (p(x), x, F(x), \text{id}_{F(x)})$ on objects and $(a : x \to x') \mapsto (a, F(a))$ on morphisms. It is clear that the composition $\mathcal{X} \to \mathcal{X}' \to \mathcal{Y}$ equals $F$. We omit the verification that $\mathcal{X} \to \mathcal{X}'$ is an equivalence of fibred categories over $\mathcal{C}$.

Finally, we have to show that $\mathcal{X}' \to \mathcal{Y}$ is a category fibred in groupoids. Let $b : y' \to y$ be a morphism in $\mathcal{Y}$ and let $(U, x, y, f)$ be an object of $\mathcal{X}'$ lying over $y$. Because $\mathcal{X}$ is fibred in groupoids over $\mathcal{C}$ we can find a morphism $a : x' \to x$ lying over $U' = q(y') \to q(y) = U$. Since $\mathcal{Y}$ is fibred in groupoids over $\mathcal{C}$ and since both $F(x') \to F(x)$ and $y' \to y$ lie over the same morphism $U' \to U$ we can find $f' : F(x') \to y'$ lying over $\text{id}_{U'}$ such that $f \circ F(a) = b \circ f'$. Hence we obtain $(a, b) : (U', x', y', f') \to (U, x, y, f)$. This verifies the first condition (1) of Definition 4.35.1. To see (2) let $(a, b) : (U', x', y', f') \to (U, x, y, f)$ and $(a', b') : (U'', x'', y'', f'') \to (U, x, y, f)$ be morphisms of $\mathcal{X}'$ and let $b'' : y' \to y''$ be a morphism of $\mathcal{Y}$ such that $b' \circ b'' = b$. We have to show that there exists a unique morphism $a'' : x' \to x''$ such that $f'' \circ F(a'') = b'' \circ f'$ and such that $(a', b') \circ (a'', b'') = (a, b)$. Because $\mathcal{X}$ is fibred in groupoids we know there exists a unique morphism $a'' : x' \to x''$ such that $a' \circ a'' = a$ and $p(a'') = q(b'')$. Because $\mathcal{Y}$ is fibred in groupoids we see that $F(a'')$ is the unique morphism $F(x') \to F(x'')$ such that $F(a') \circ F(a'') = F(a)$ and $q(F(a'')) = q(b'')$. The relation $f'' \circ F(a'') = b'' \circ f'$ follows from this and the given relations $f \circ F(a) = b \circ f'$ and $f \circ F(a') = b' \circ f''$. $\square$