The Stacks project

Proof. Let $(V, U', \varphi )$ be an object of the fibre product category. Set $U = U' \times _{X'} X$. Note that $U \to U'$ is a thickening. Since $\varphi : V \times _ Y X \to U' \times _{X'} X = U$ is an isomorphism we have a morphism $U \to V$ over $X \to Y$ which identifies $U$ with the fibre product $X \times _ Y V$. In particular $U \to V$ is affine, see Morphisms, Lemma 29.11.8. Hence we can apply Lemma 37.14.3 to get a pushout $V' = V \amalg _ U U'$. Denote $V' \to Y'$ the morphism we obtain in virtue of the fact that $V'$ is a pushout and because we are given morphisms $V \to Y$ and $U' \to X'$ agreeing on $U$ as morphisms into $Y'$. Setting $G(V, U', \varphi ) = V'$ gives the functor $G$.

Let us prove that $G$ is a left adjoint to $F$. Let $Z$ be a scheme over $Y'$. We have to show that

where the morphism sets are taking in their respective categories. Let $g' : V' \to Z$ be a morphism. Denote $\tilde g$, resp. $\tilde f'$ the composition of $g'$ with the morphism $V \to V'$, resp. $U' \to V'$. Base change $\tilde g$, resp. $\tilde f'$ by $Y \to Y'$, resp. $X' \to Y'$ to get a morphism $g : V \to Z \times _{Y'} Y$, resp. $f' : U' \to Z \times _{Y'} X'$. Then $(g, f')$ is an element of the right hand side of the equation above (details omitted). Conversely, suppose that $(g, f') : (V, U', \varphi ) \to F(Z)$ is an element of the right hand side. We may consider the composition $\tilde g : V \to Z$, resp. $\tilde f' : U' \to Z$ of $g$, resp. $f$ by $Z \times _{Y'} X' \to Z$, resp. $Z \times _{Y'} Y \to Z$. Then $\tilde g$ and $\tilde f'$ agree as morphism from $U$ to $Z$. By the universal property of pushout, we obtain a morphism $g' : V' \to Z$, i.e., an element of the left hand side. We omit the verification that these constructions are mutually inverse.

To prove that $F \circ G$ is isomorphic to the identity we have to show that the adjunction mapping $(V, U', \varphi ) \to F(G(V, U', \varphi ))$ is an isomorphism. To do this we may work affine locally. Say $X = \mathop{\mathrm{Spec}}(A)$, $X' = \mathop{\mathrm{Spec}}(A')$, and $Y = \mathop{\mathrm{Spec}}(B)$. Then $A' \to A$ and $B \to A$ are ring maps as in More on Algebra, Lemma 15.6.4 and $Y' = \mathop{\mathrm{Spec}}(B')$ with $B' = B \times _ A A'$. Next, suppose that $V = \mathop{\mathrm{Spec}}(D)$, $U' = \mathop{\mathrm{Spec}}(C')$ and $\varphi $ is given by an $A$-algebra isomorphism $D \otimes _ B A \to C' \otimes _{A'} A = C'/IC'$. Set $D' = D \times _{C'/IC'} C'$. In this case the statement we have to prove is that $D' \otimes _{B'} B \cong D$ and $D' \otimes _{B'} A' \cong C'$. This is a special case of More on Algebra, Lemma 15.6.4. $\square$