**Proof.**
Consider the naive cotangent complex of the given presentation

\[ (f_1, \ldots , f_ c)/(f_1, \ldots , f_ c)^2 \longrightarrow \bigoplus \nolimits _{i = 1}^ n S \text{d}x_ i \]

Let us compose this map with the projection onto the first $c$ direct summands of the direct sum. According to the definition of a standard smooth algebra the classes $f_ i \bmod (f_1, \ldots , f_ c)^2$ map to a basis of $\bigoplus _{i = 1}^ c S\text{d}x_ i$. We conclude that $(f_1, \ldots , f_ c)/(f_1, \ldots , f_ c)^2$ is free of rank $c$ with a basis given by the elements $f_ i \bmod (f_1, \ldots , f_ c)^2$, and that the homology in degree $0$, i.e., $\Omega _{S/R}$, of the naive cotangent complex is a free $S$-module with basis the images of $\text{d}x_{c + j}$, $j = 1, \ldots , n - c$. In particular, this proves $R \to S$ is smooth.

The proofs of (4) and (6) are omitted. But see the example below and the proof of Lemma 10.135.10.

Let $\varphi : R \to R'$ be any ring map. Denote $S' = R'[x_1, \ldots , x_ n]/(f_1^\varphi , \ldots , f_ c^\varphi )$ where $f^\varphi $ is the polynomial obtained from $f \in R[x_1, \ldots , x_ n]$ by applying $\varphi $ to all the coefficients. Then $S' \cong R' \otimes _ R S$. Moreover, the determinant of Definition 10.136.6 for $S'/R'$ is equal to $g^\varphi $. Its image in $S'$ is therefore the image of $g$ via $R[x_1, \ldots , x_ n] \to S \to S'$ and hence invertible. This proves (5).

To prove (7) it suffices to show that $S \otimes _ R \kappa (\mathfrak p)$ has dimension $n - c$ for every prime $\mathfrak p \subset R$. By (5) it suffices to prove that any standard smooth algebra $k[x_1, \ldots , x_ n]/(f_1, \ldots , f_ c)$ over a field $k$ has dimension $n - c$. We already know that $k[x_1, \ldots , x_ n]/(f_1, \ldots , f_ c)$ is a local complete intersection by Lemma 10.136.5. Hence, since $I/I^2$ is free of rank $c$ we see that $k[x_1, \ldots , x_ n]/(f_1, \ldots , f_ c)$ has dimension $n - c$, by Lemma 10.134.4 for example.
$\square$

## Comments (2)

Comment #2824 by Dario Weißmann on

Comment #2925 by Johan on