Fix error in proof lemma

Thanks to 李一笑 who wrote

"In the proof of lemma 0241, one applies $\phi'$ to $(v_i,x_j)$, which
may not be a well defined $V' \times_{S'} X'$-point."

Unfortunately, the lemma wasn't fixable and we needed to change the
statement of the lemmma as well.

A counter example to the original statement of the lemma is for example
given by taking a nonempty scheme S and taking both X and S' to be two
disjoint copies of S mapping to S and finally taking both V and W to be
two copies of X mapping to X with the descent datum that produces
again two copies of S mapping to S when you descend V and W along X
mapping to S. Then you see that a morphism of descent data from V' to W'
just comes down to a morphism of two copies of S' over S' to two copies
of S' over S' which doesn't always descend to a corresponding morphism
over S... (This is just to remind me what went wrong; when I wrote this
I must have thought that the condition that X' x_{S'} X' ---> X x_S X
would prevent this kind of thing, but it was obviously garbage.)
 @@ -7796,8 +7796,7 @@ \section{Fully faithfulness of the pullback functors} \begin{enumerate} \item $\{f : X' \to X\}$ is an fpqc covering (for example if $f$ is surjective, flat, and quasi-compact), and \item $f \times f : X' \times_{S'} X' \to X \times_S X$ is surjective and flat\footnote{This follows from (1) if $S = S'$.}. \item $S = S'$. \end{enumerate} Then the pullback functor is fully faithful. \end{lemma} @@ -7809,7 +7808,7 @@ \section{Fully faithfulness of the pullback functors} Let $(V, \varphi)$ and $(W, \psi)$ be two descent data relative to $X \to S$. Set $(V', \varphi') = f^*(V, \varphi)$ and $(W', \psi') = f^*(W, \psi)$. Let $\alpha' : V' \to W'$ be a morphism of descent data for $X'$ over $S'$. Let $\alpha' : V' \to W'$ be a morphism of descent data for $X'$ over $S$. We have to show there exists a morphism $\alpha : V \to W$ of descent data for $X$ over $S$ whose pullback is $\alpha'$. @@ -7820,10 +7819,10 @@ \section{Fully faithfulness of the pullback functors} By assumption the diagram $$\xymatrix{ V' \times_{S'} X' \ar[r]_{\varphi'} \ar[d]_{\alpha' \times \text{id}} & X' \times_{S'} V' \ar[d]^{\text{id} \times \alpha'} \\ W' \times_{S'} X' \ar[r]^{\psi'} & X' \times_{S'} W' V' \times_S X' \ar[r]_{\varphi'} \ar[d]_{\alpha' \times \text{id}} & X' \times_S V' \ar[d]^{\text{id} \times \alpha'} \\ W' \times_S X' \ar[r]^{\psi'} & X' \times_S W' }$$ commutes. We claim the two compositions @@ -7860,7 +7859,7 @@ \section{Fully faithfulness of the pullback functors} ((x_i, x_j), \psi(u_i, x)) = ((x_i, x_j), (x, u'_j)) $$as points of (X' \times_{S'} X') \times_{X \times_S X} (X \times_S W) (X' \times_S X') \times_{X \times_S X} (X \times_S W) for all i, j \in \{0, 1\}. This shows that \psi(u_0, x) = \psi(u_1, x) and hence u_0 = u_1 by taking \psi^{-1}. This proves the claim because the argument above was formal @@ -7884,8 +7883,8 @@ \section{Fully faithfulness of the pullback functors} W \times_S X \ar[r]^{\psi} & X \times_S W }$$ commutes because its base change to $X' \times_{S'} X'$ commutes and the morphism $X' \times_{S'} X' \to X \times_S X$ commutes because its base change to $X' \times_S X'$ commutes and the morphism $X' \times_S X' \to X \times_S X$ is surjective and flat (use Lemma \ref{lemma-ff-base-change-faithful}). Hence $\alpha$ is a morphism of descent data $(V, \varphi) \to (W, \psi)$ as desired.