The Stacks project

Proof. Since $U \to S$ is locally of finite type (as a composition of such morphisms), we see that $\mathop{\mathrm{Spec}}(k) \to S$ is of finite type (again as a composition). Thus the statement makes sense. The equivalence of (1) and (2) is the definition of $x$ being versal at $u_0$. The equivalence of (1) and (3) is Artin's Axioms, Lemma 98.12.3. Thus (1), (2), and (3) are equivalent.

If $x|_{U'}$ is smooth, then the functor $\hat x : \mathcal{F}_{U, k, u_0} \to \mathcal{F}_{\mathcal{X}, k, x_0}$ is smooth by Artin's Axioms, Lemma 98.3.2. Thus (4) implies (1), (2), and (3). For the converse, assume $x$ is versal at $u_0$. Choose a surjective smooth morphism $y : V \to \mathcal{X}$ where $V$ is a scheme. Set $Z = V \times _\mathcal {X} U$ and pick a finite type point $z_0 \in |Z|$ lying over $u_0$ (this is possible by Morphisms of Spaces, Lemma 67.25.5). By Artin's Axioms, Lemma 98.12.6 the morphism $Z \to V$ is smooth at $z_0$. By definition we can find an open neighbourhood $W \subset Z$ of $z_0$ such that $W \to V$ is smooth. Since $Z \to U$ is open, let $U' \subset U$ be the image of $W$. Then we see that $U' \to \mathcal{X}$ is smooth by our definition of smooth morphisms of stacks.

The final statement follows from the definitions as $\mathcal{O}_{U, u_0}^\wedge$ prorepresents $\mathcal{F}_{U, k, u_0}$. $\square$