The Stacks project

Proof. Let $k \to R$ be a ring map where $k$ is a field and $R$ a Noetherian ring. Assume $P(k \to R)$ is true. Let $K/k$ be a finitely generated field extension. By Algebra, Lemma 10.45.3 we can find a diagram

where $k'/k$, $K'/K$ are finite purely inseparable field extensions such that $K'/k'$ is separable. By Algebra, Lemma 10.158.10 there exists a smooth $k'$-algebra $B$ such that $K'$ is the fraction field of $B$. Now we can argue as follows: Step 1: $R \otimes _ k k'$ satisfies $(S_ n)$ because we assumed $P$ for $k \to R$. Step 2: $R \otimes _ k k' \to R \otimes _ k k' \otimes _{k'} B$ is a smooth ring map (Algebra, Lemma 10.137.4) and we conclude $R \otimes _ k k' \otimes _{k'} B$ satisfies $(S_ n)$ by Algebra, Lemma 10.163.5 (and using Algebra, Lemma 10.140.3 to see that the hypotheses are satisfied). Step 3. $R \otimes _ k k' \otimes _{k'} K' = R \otimes _ k K'$ satisfies $(R_ n)$ as it is a localization of a ring having $(R_ n)$. Step 4. Finally $R \otimes _ k K$ satisfies $(R_ n)$ by descent of $(R_ n)$ along the faithfully flat ring map $K \otimes _ k A \to K' \otimes _ k A$ (Algebra, Lemma 10.164.6). This proves (A). Part (B) follows too: a Noetherian ring has $(R_ n)$ if and only if all of its local rings have $(R_ n)$. Part (C). This follows from Algebra, Lemma 10.163.5 as the fibres of a regular homomorphism are regular (small detail omitted). Part (D). This follows from Algebra, Lemma 10.164.6 (small detail omitted).

Part (E). Let $l/k$ be a separable algebraic extension of fields and let $l \to R$ be a ring map with $R$ Noetherian. Assume that $k \to R$ has $P$. We have to show that $l \to R$ has $P$. Let $l'/l$ be a finite extension. First observe that there exists a finite subextension $l/m/k$ and a finite extension $m'/m$ such that $l' = l \otimes _ m m'$. Then $R \otimes _ l l' = R \otimes _ m m'$. Hence it suffices to prove that $m \to R$ has property $P$, i.e., we may assume that $l/k$ is finite. If $l/k$ is finite, then $l'/k$ is finite and we see that

is a localization (by Algebra, Lemma 10.43.8) of the Noetherian ring $l' \otimes _ k R$ which has property $(R_ n)$ by assumption $P$ for $k \to R$. This proves that $l' \otimes _ l R$ has property $(R_ n)$ as desired. $\square$