In an attempt to prove that polynomial ring of a regular ring is a regular ring, I encounter this beautiful result
"$R$ is a local Noetherian ring. $Q\in \operatorname{Spec}(R[X])$ and $P=Q\cap R$. Then $R_P\to R[X]_Q$ is flat local and $(R[X]/PR[X])_Q$ is a regular local ring"
I can only prove the above homomorphism is local, which is evident. Can you help me solve the other two properties? THank you
Hint 1:
$R[X]_\mathfrak{q}\simeq \bigl(R_\mathfrak{p}[X]\bigr)_\mathfrak{q}$, so the morphism $\;R_\mathfrak{p}\longrightarrow\bigl(R_\mathfrak{p}[X]\bigr)_\mathfrak{q} $ is the composition of $\;R_\mathfrak{p}\longrightarrow R_\mathfrak{p}[X] $, which is a free $R_\mathfrak{p}$-module, with the canonical morphism $\;R_\mathfrak{p}[X]\longrightarrow \bigl(R_\mathfrak{p}[X]\bigr)_\mathfrak{q} $, which is flat.
Hint 2:
$\bigl(R[X]/\mathfrak pR[X]\bigr)_{\mathfrak q}\simeq \bigl((R_\mathfrak{p}[X]/\mathfrak pR_\mathfrak{p})[X]\bigr)_{\mathfrak q}= \bigl(k(\mathfrak p)[X]\bigr)_\mathfrak{q} $ is a localisation of the polynomial ring over the residual field $k(\mathfrak p)$.