The Stacks project

Proof. Let us prove the functor is essentially surjective. Let $U' \to X_{k'}$ be a finite étale morphism. Write $k' = \mathop{\mathrm{colim}}\nolimits A_ i$ as a filtered colimit of finite type $k$-algebras. By Limits, Lemma 32.10.1 there exists an $i$ and a finitely presented morphism $U_ i \to X_{A_ i}$ whose base change to $X_{k'}$ is $U'$. After increasing $i$ we may assume that $U_ i \to X_{A_ i}$ is finite and étale (Limits, Lemmas 32.8.3 and 32.8.10). Since $k$ is algebraically closed we can find a $k$-valued point $t$ in $\mathop{\mathrm{Spec}}(A_ i)$. Let $U = (U_ i)_ t$ be the fibre of $U_ i$ over $t$. Let $A_ i^ h$ be the henselization of $(A_ i)_{\mathfrak m}$ where $\mathfrak m$ is the maximal ideal corresponding to the point $t$. By Lemma 58.9.1 we see that $(U_ i)_{A_ i^ h} = U \times \mathop{\mathrm{Spec}}(A_ i^ h)$ as schemes over $X_{A_ i^ h}$. Now since $A_ i^ h$ is algebraic over $A_ i$ (see for example discussion in Smoothing Ring Maps, Example 16.13.3) and since $k'$ is algebraically closed we can find a ring map $A_ i^ h \to k'$ extending the given inclusion $A_ i \subset k'$. Hence we conclude that $U'$ is isomorphic to the base change of $U$. The proof of fully faithfulness is exactly the same. $\square$