Lemma 15.38.5. Let $k$ be a field. Let $(A, \mathfrak m, K)$ be a regular local $k$-algebra such that $K/k$ is separable. Then $k \to A$ is formally smooth in the $\mathfrak m$-adic topology.

Proof. It suffices to prove that the completion of $A$ is formally smooth over $k$, see Lemma 15.37.4. Hence we may assume that $A$ is a complete local regular $k$-algebra with residue field $K$ separable over $k$. By Lemma 15.38.4 we see that $A = K[[x_1, \ldots , x_ n]]$.

The power series ring $K[[x_1, \ldots , x_ n]]$ is formally smooth over $k$. Namely, $K$ is formally smooth over $k$ and $K[x_1, \ldots , x_ n]$ is formally smooth over $K$ as a polynomial algebra. Hence $K[x_1, \ldots , x_ n]$ is formally smooth over $k$ by Algebra, Lemma 10.138.3. It follows that $k \to K[x_1, \ldots , x_ n]$ is formally smooth for the $(x_1, \ldots , x_ n)$-adic topology by Lemma 15.37.2. Finally, it follows that $k \to K[[x_1, \ldots , x_ n]]$ is formally smooth for the $(x_1, \ldots , x_ n)$-adic topology by Lemma 15.37.4. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).