The Stacks project

Proof. This translates into the following algebra fact. Let $A \to B$ be a finite type homomorphism of rings of characteristic $p$. Set $B' = B \otimes _{A, F_ A} A$ and consider the ring map $F_{B/A} : B' \to B$, $b \otimes a \mapsto b^ pa$. Then our assertion is that $F_{B/A}$ is finite. Namely, if $x_1, \ldots , x_ n \in B$ are generators over $A$, then $x_ i$ is integral over $B'$ because $x_ i^ p = F_{B/A}(x_ i \otimes 1)$. Hence $F_{B/A} : B' \to B$ is finite by Algebra, Lemma 10.36.5. $\square$