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?
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 semilocal noetherian rings due to $K$ being finite separable over $k$). QED

$\begingroup$ I changed "kvariety" to "regular scheme of finite type" as you suggested. $\endgroup$ Dec 16 '13 at 17:33

$\begingroup$ Can you please explain a little more the last step of your proof? (the finite separable case) $\endgroup$ Dec 16 '13 at 17:34

1$\begingroup$ @Tomasz Lenarcik: If $R$ is a regular local $k$algebra of dimension $d$ (e.g., localize $A$ at a prime), $\{t_1,\dots,t_d\}$ generates its maximal ideal $m$, and $K$ is finite separable over $k$, then $K\otimes_k (R/m)$ is a finite direct product of fields: residue fields at maximal ideals of the semilocal $K\otimes_k R$. Thus, $\{t_1,\dots, t_d\}$ generates each local ring of $K\otimes_k R$ at a maximal ideal (!). Those local rings have dimension $d$ (since $K\otimes_k R$ is finite flat over $R$), so they're regular. In fancier terms, an etale algebra over a regular ring is regular. $\endgroup$ Dec 17 '13 at 2:48
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.

$\begingroup$ To provide relevant references in Matsumura's "Commutative Ring Theory" (EGA 0$_{\rm{IV}}$, 19.519.6 is similar, but with heavier style), the "i.e." is Thm 26.9 and by flatness of $A\rightarrow A\otimes_k K$ and regularity of $A$ it suffices (by dimension formula for flat local maps; see Thm 23.7(ii)) to prove regularity of local rings of the noetherian fiber algebras. A local noetherian ring $(R,m)$ formally smooth for the discrete topology over a field $F$ is formally $F$smooth for its $m$adic topology, so conclude via Cohen's work on coefficient fields: Thm 28.3 and subsequent Lemma 1. $\endgroup$ Dec 17 '13 at 13:55

$\begingroup$ So this approach is more elementary than my answer since it doesn't use Serre's theorem, and only requires some basic properties of flatness and results known in the prehomological era (though of course the viewpoint of formal smoothness only came along later). $\endgroup$ Dec 17 '13 at 13:58