Let $k\subset K$ be a separable field extension. As a particular case of M. André [Localisation de la lissité formelle](https://link.springer.com/article/10.1007%2FBF01168230) one obtains that the natural inclusion of power series rings $k[[X\_1,\ldots,X\_n]]\subset K[[X\_1,\ldots,X\_n]]$ is regular. Is there an alternative (simpler) argument that works in this particular case?



Proving that a morphism between power series rings is regular
I believe the following works, as long as by "separable" you mean "separable algebraic." I will denote $K$ by $L$ to make $k$ and $K$ more distinct.


*Proof.* Consider the factorization
$$k[[X\_1,\ldots,X\_n]] \subseteq L \otimes\_k k[[X\_1,\ldots,X\_n]] \subseteq L[[X\_1,\ldots,X\_n]].\tag{1}\label{eq:factor}$$
Since regular homomorphisms are stable under composition [[EGAIV$\_2$](http://www.numdam.org/item/PMIHES_1965__24__5_0/), Proposition 6.6.1(i); Stacks, [Tag 07QI](https://stacks.math.columbia.edu/tag/07QI)] it suffices to show that each homomorphism in this factorization is regular.


The first homomorphism is the direct limit of module-finite smooth homomorphisms
$$k[[X\_1,\ldots,X\_n]] \subseteq k\_\alpha \otimes\_k k[[X\_1,\ldots,X\_n]],\tag{2}\label{eq:kalpha}$$
where $k \subseteq k\_\alpha$ ranges over all finite separable subextensions of $k \subseteq L$. Since $k \subseteq k\_\alpha$ is smooth, the homomorphisms \eqref{eq:kalpha} are also smooth by base change [[EGAIV$\_2$](http://www.numdam.org/item/PMIHES_1965__24__5_0/), Proposition 6.8.3(iii); Stacks, [Tag 00T4](https://stacks.math.columbia.edu/tag/00T4)]. Thus, the first homomorphism in \eqref{eq:factor} is regular by the easy direction of Néron–Popescu desingularization [[Swan](https://mathscinet.ams.org/mathscinet-getitem?mr=1697953), Lemma 1.4; Stacks, [Tag 07EP](https://stacks.math.columbia.edu/tag/07EP)].


We now show that the second homomorphism in \eqref{eq:factor} is regular. Since this homomorphism can be identified with the $(X\_1,\ldots,X\_n)$-adic completion of $L \otimes\_k k[[X\_1,\ldots,X\_n]]$, it suffices to show that $L \otimes\_k k[[X\_1,\ldots,X\_n]]$ is a $G$-ring. This follows by adapting the proof that the strict henselization of a Noetherian local $G$-ring is a $G$-ring [Stacks, [Tag 07QR](https://stacks.math.columbia.edu/tag/07QR)]. $\blacksquare$


One can also adapt the strategy of [this comment](https://mathoverflow.net/questions/199416/are-the-fibers-of-this-morphism-geometrically-regular?rq=1#comment495228_199416) by user74230 to a [similar question](https://mathoverflow.net/q/199416/33088). One first replaces $L$ by the separable closure $k^{\mathrm{sep}}$ of $k$, in which case it suffices to show $k[[X\_1,\ldots,X\_n]] \subseteq k^{\mathrm{sep}}[[X\_1,\ldots,X\_n]]$ is regular by the fact that $L[[X\_1,\ldots,X\_n]] \subseteq k^{\mathrm{sep}}[[X\_1,\ldots,X\_n]]$ is faithfully flat [Stacks, [Tag 07NT](https://stacks.math.columbia.edu/tag/07NT)]. Now the argument in [the comment referenced above](https://mathoverflow.net/questions/199416/are-the-fibers-of-this-morphism-geometrically-regular?rq=1#comment495228_199416) applies.


