The Stacks project

Proof. The equivalence of (2) and (3) follows immediately from Formal Deformation Theory, Lemma 90.9.4.

Note that $\mathcal{O}_{S, s} \to A$ is formally smooth in the $\mathfrak m_ A$-adic topology if and only if $\mathcal{O}_{S, s} \to A' = A[[t_1, \ldots , t_ r]]$ is formally smooth in the $\mathfrak m_{A'}$-adic topology. Hence (2) does not depend on the choice of our versal ring by Lemma 107.2.4. Next, let $l/k$ be a finite extension and choose $A \to A'$ as in Lemma 107.2.5. If $\mathcal{O}_{S, s} \to A$ is formally smooth in the $\mathfrak m_ A$-adic topology, then $\mathcal{O}_{S, s} \to A'$ is formally smooth in the $\mathfrak m_{A'}$-adic topology, see More on Algebra, Lemma 15.37.7. Conversely, if $\mathcal{O}_{S, s} \to A'$ is formally smooth in the $\mathfrak m_{A'}$-adic topology, then $\mathcal{O}_{S, s}^\wedge \to A'$ and $A \to A'$ are regular (More on Algebra, Proposition 15.49.2) and hence $\mathcal{O}_{S, s}^\wedge \to A$ is regular (More on Algebra, Lemma 15.41.7), hence $\mathcal{O}_{S, s} \to A$ is formally smooth in the $\mathfrak m_ A$-adic topology (same lemma as before). Thus the equivalence of (2) and (1) holds for $k$ and $x_0$ if and only if it holds for $l$ and $x_{0, l}$.

Choose a scheme $U$ and a smooth morphism $U \to \mathcal{X}$ such that $\mathop{\mathrm{Spec}}(k) \times _\mathcal {X} U$ is nonempty. Choose a finite extension $l/k$ and a point $w_0 : \mathop{\mathrm{Spec}}(l) \to \mathop{\mathrm{Spec}}(k) \times _\mathcal {X} U$. Let $u_0 \in U$ be the image of $w_0$. We may apply the above to $l/k$ and to $l/\kappa (u_0)$ to see that we can reduce to $u_0$. Thus we may assume $A = \mathcal{O}_{U, u_0}^\wedge $, see Lemma 107.2.6. Observe that $x_0$ is in the smooth locus of $\mathcal{X} \to S$ if and only if $u_0$ is in the smooth locus of $U \to S$, see for example Morphisms of Stacks, Lemma 101.33.6. Thus the equivalence of (1) and (2) follows from More on Algebra, Lemma 15.38.6. $\square$