Geometric regularity for infinitely generated field extensions

Question

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

1. $A\otimes_k k'$ is a regular ring for all finitely generated field extensions $k\subset k'$.
2. $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.

Answer 1

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$