The Stacks project

Doesn't this work for any regular ring and any polynomial of the form $p+f$ where $p\in \mathbf{Z}[z]$ is regarded as a polynomial in $R[z]$?

A reference to the fact that a polynomial algebra over a regular ring is regular would be nice. I can't find it in the project so here is what I came up with (compiles fine for me but not as a comment?): Let $R$ be a regular ring. To show that $R[z]$ is a regular ring it suffices to show that the localization at all maximal ideals of $R[z]$ are regular local rings. Let $\mathfrak{m}$ be a maximal ideal of $R[z]$. Write $\mathfrak{p}=R\cap \mathfrak{m}$. Then $R[z]_{\mathfrak{m}}=R_{\mathfrak{p}}[z]_{\mathfrak{m}}$ and we can reduce to $R$ is a regular local ring, $\mathfrak{m}$ is a maximal ideal of $R[z]$ lying over $\mathfrak{m}_R$. Then $R[z]/\mathfrak{m}=\kappa[z]/\overline{\mathfrak{m}}$ is a field where $\overline{\mathfrak{m}}$ denotes the image of $\mathfrak{m}$ in $\kappa[z]$. Let $\overline{f}\in \kappa[z]$ be a generator of $\overline{\mathfrak{m}}$ and $f\in R[z]$ be a lift. Further let $f_1,\dots,f_r$ be a regular sequence in $R$ generating the maximal ideal. Then $f_1,\dots,f_r,f$ defines a regular sequence in $R[z]_{\mathfrak{m}}$ generating $\mathfrak{m}$.

OK, so it only didn't compile in the preview?

The preview and the final render are dealt with by different pieces of the software, but of course they should be as close together as possible. I'll see what I can do to improve this in the future, thanks for telling me about it.

Any smooth algebra over a regular ring is regular, see 10.163.10. The proof is essentially what you said in the case of polynomial rings.

Unfortunately, I don't understand your first comment. Can you clarify?

So the proof works by lemma 07PF for any polynomial mapping to a unit in R[z] under some derivation. We have $D(z^k)=kz^{k-1}D(z)=0$ by definition of $D$. By linearity the same is true for any polynomial $p$ with integer coefficients regarded as a polynomial in $R[z]$ via $\mathbf{Z}[z]\to R[z]$. So $D(p+f)=D(f)$ is a unit in $R[z]$.

We didn't need the $\mathbf{F}_p$-algebra structure and it holds for a larger class of polynomials.

Thank you for the reference!

OK, I understand now. Thank you. I will change the lemma when I next go through the comments.

OK, I have added this in this commit.