Does regular field extension preserve regularity? Let $k$ be an arbitrary field and suppose that $K/k$ is a regular field extension. Let $V$ be regular scheme of finite type over $\text{Spec }k$ (not necessarily smooth). Is it true that $\text{Spec }K\times_{\text{Spec }k}V$ is also regular?
 A: Yes, and it is only necessary to assume $K$ is separable over $k$ (i.e., not necessary to assume in addition that $k$ is algebraically closed in $K$).  The idea is to use Serre's regularity criterion to reduce to the case when $K/k$ is  finitely generated, and then use a separating transcendence basis in such cases to conclude.
In more detail, write $K = \varinjlim K_i$ for subfields $K_i$ finitely generated over $k$, so all $K_i$ inherit $k$-separability from $K$.  We may assume $V$ is affine, say $V = {\rm{Spec}}(A)$. Clearly $K \otimes_k A = \varinjlim (K_i \otimes_k A)$, so for any prime ideal $P$ of $K \otimes_k A$ we have
$$(K \otimes_k A)_P = \varinjlim (K_i \otimes_k A)_{P_i}$$
where $P_i$ is the contraction of $P$ along $K_i \otimes_k A \rightarrow K \otimes_k A$.  Let $M$ be a finitely generated module over 
$(K \otimes_k A)_P$ for a prime ideal $P$ of $K \otimes_k A$, so it is also finitely presented since $(K \otimes_k A)_P$ is noetherian (as $A$ is finitely generated over $k$).  For ease of notation, let $R = (K \otimes_k A)_P$ and let $R_i = (K_i \otimes_k A)_{P_i}$ for all $i$, so $\{R_i\}$ is a directed system of local rings with direct limit $R$.  Note that the transition maps in this directed system are flat, and $\dim R_i, \dim R \le \dim(A)$.
Since $M$ is finitely presented over $R$, clearly 
$M = R \otimes_{R_{i_0}} M_0$ for some $i_0$ and a finitely generated $R_{i_0}$-module $M_0$.  Assume the case of finitely generated separable extensions is settled, so the local noetherian ring $R_{i_0}$ is regular, visibly with dimension at most $\dim(A)$. Hence, $M_0$ admits a finite projective resolution over $R_{i_0}$ of length at most $\dim(A)$ by Serre's criterion.  Applying the exact functor $R \otimes_{R_{i_0}} (\cdot)$ to this yields a finite projective resolution of $M$ over $R$ of length at most $\dim(A)$.  Thus, the local noetherian ring $R = (K \otimes_k A)_P$ has finite global dimension (at most $\dim(A)$) since $M$ was arbitrary, so $R$ is regular by Serre's criterion.  Since $P$ was arbitrary, it follows (by definition) that $K \otimes_k A$ is regular. This completes the reduction to the case when $K$ is finitely generated over $k$.
Now we may and do assume $K$ is finitely generated over $k$, so via the existence of a separating transcendence basis we reduce to the two special cases that $K = k(x_1,\dots,x_n)$ or $K$ is finite separable over $k$. In the first case, $K \otimes_k A$ is a localization of $A[x_1,\dots,x_n]$, and this polynomial ring is regular (since it is $A$-flat with fiber algebras over $A$ that are regular and even polynomial rings over fields), so $K \otimes_k A$ is regular.  In the second case one can conclude via the original definition of regularity via regular systems of parameters (any regular system of parameters in the local ring of $A$ at a prime $P$ is also a regular system of parameters in the local ring of $K \otimes_k A$ in any prime over $P$ since $K \otimes_k (\cdot)$ commutes with the formation of Jacobson radicals in semi-local noetherian rings due to $K$ being finite separable over $k$). QED
A: If $k \rightarrow K$ is formally smooth for the discrete topology (i.e. separable), by flat base change $A \rightarrow A\otimes_kK$ is formally smooth for any $k$-algebra $A$ essentially of finite type, and so, if $A$ is regular then $A\otimes_kK$ is regular.
