Proving that a morphism between power series rings is regular

Question

Let $k\subset K$ be a separable field extension. As a particular case of M. André Localisation de la lissité formelle 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?

Answer 1

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$, Proposition 6.6.1(i); Stacks, 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$, Proposition 6.8.3(iii); Stacks, Tag 00T4]. Thus, the first homomorphism in \eqref{eq:factor} is regular by the easy direction of Néron–Popescu desingularization [Swan, Lemma 1.4; Stacks, 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]. $\blacksquare$

One can also adapt the strategy of this comment by user74230 to a similar question. 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]. Now the argument in the comment referenced above applies.