Geometric regularity for infinitely generated field extensions Let $k$ be a field. Suppose that for a finite type $k$-algebra $A$, we define two following properties:


*

*$A\otimes_k k'$ is a regular ring for all finitely generated field extensions $k\subset k'$. 

*$A\otimes_k k'$ is a regular ring for all field extensions $k\subset k'$. 


Are these two properties equivalent? In other words, is the failure to be geometrically regular witnessed by a finitely generated field extension?
Note that the second definition makes sense because the base change of a finite type algebra is finite type (so Noetherian, in particular). Definitions are those used in Stacks project, in the case it matters. 
 A: I think the following argument works.
(2) $\Rightarrow$ (1) is clear, and so it suffices to show the converse. Let $k \subset K$ be an arbitrary field extension; we want to show that $A \otimes_k K$ is regular assuming the condition in (1).
We have the following:
Proposiition [EGAIV$_2$, Prop. 5.13.7]. Let $\{(A_\alpha,\varphi_{\beta\alpha})\}$ be a filtered direct system of rings and set $A = \varinjlim A_\alpha$. Suppose that $A_\alpha$ is regular for every $\alpha$, and that $\varphi_{\beta\alpha}$ is flat for every $\alpha \le \beta$. If $A$ is noetherian, then $A$ is regular.
Now write $K$ as the direct limit $\varinjlim k_\alpha$ of the filtered direct system of finitely generated subfield extensions $k \subset k_\alpha$ of $K$ with transition homomorphisms $\varphi_{\beta\alpha}$. Then, for every $\alpha$, the ring $A \otimes_k k_\alpha$ is regular by assumption in (1). Note that the induced directed system $\{(A \otimes_k k_\alpha,\mathrm{id}_A \otimes_k \varphi_{\beta\alpha})\}$ has flat transition homomorphisms by base change. Since
$$A \otimes_k K \simeq A \otimes_k \varinjlim k_\alpha \simeq \varinjlim \bigl(A \otimes_k k_\alpha\bigr),$$
the proposition therefore implies that $A \otimes_k K$ is regular. $\blacksquare$
