Remark 1

Corollaries 1 and 2 apply in particular when $k_0$ is a field and one is in one of the following two cases: a) $B$ is an algebra essentially of finite type over a separable extension of $k_0$ (th. 1 of No. 3); b) $B$ is a complete noetherian local $k_0$-algebra whose residue field $\kappa_B$ is a separable extension of $k_0$ (in this case one takes for $k$ an algebra of formal power series over $\kappa_B$ of which $B$ is a quotient (No. 3 and IX, § 3, No. 3)). In each of these cases, it follows from cor. 2, having regard to prop. 8 of No. 7 and prop. 6, b) of § 6, No. 4, that the $k_0$-algebra $B$ is formally smooth if and only if it is absolutely regular.

Corollary 3 (Zariski). — Let $k$ be a field, $A$ a regular local $k$-algebra, and $J$ an ideal of $A$ distinct from $A$. Suppose that the $k$-algebra $A$ is essentially of finite type or complete. In order that the local ring $A/J$ be regular, it is necessary and sufficient that there exist an integer $m \geqslant 0$, elements $f_1, \ldots, f_m$ of $J$ generating $J$, and derivations $D_1, \ldots, D_m$ of $A$ such that $\det(D_j(f_i)) \notin \mathfrak{m}_A$. The elements $(f_1, \ldots, f_m)$ then form part of a system of coordinates of $A$ and the ideal $J$ is prime.

Let $k_0$ be the prime subfield of $k$. The $k_0$-algebra $A$ is absolutely regular ($§ 6$, No. 4, example 1), hence formally smooth (remark 1 above). For the same reasons, to say that $A/J$ is regular is equivalent to saying that it is a formally smooth $k_0$-algebra. The first assertion therefore follows from th. 3, which also implies that the sequence $(f_1, \ldots, f_m)$ is completely secant for $A$. One then applies prop. 2 of VIII, $§ 5$, No. 3.