Showing if $R$ is a PID and $0\neq r\in R$ is irreducible, then $R[X]/(r)\cong (R/(r))[X]$

Question

I've been looking at the statements I found on these two Stack Exchange answers and I've been trying to prove them. The first claim is:

If $R$ is a PID and $0\neq r\in R$ is irreducible, then $R[X]/(r)\cong (R/(r))[X]$

The second claim follows from the first:

If $k$ is a field, and $p(X)$ is an irreducible in $k[X]$, then $K[X,Y]/(p(X)) \cong (K[X]/(p(X)))[Y]$

Attempt to prove claim 1: It looks like I can prove this using the First Isomorphism Theorem by finding a ring morphism $R[X] \hookrightarrow (R/(r))[X]$ with $(r)$ as the kernel. However the only one I can think of is the following:

Let $f:R\rightarrow R/(r)$ be the projection $f(x)=\bar{x}$. Then we have the morphism of rings $\phi:R[X]\rightarrow (R/(r))[X]$ with the kernel $(r)[X]$ described as $\phi(a_nx^n+\cdots+a_1x+a_0)=\phi(a_nx^n)+\cdots+\phi(a_1x)+\phi(a_0)$ $=f(a_n)x^n+\cdots+f(a_1)x+f(a_0)=\bar{a_n}x^n+\cdots+\bar{a_1}x+\bar{a_0}$

Any help to prove this is appreciated!

edit: Further comment that I am interested whether the isomorphism hold only when $R$ is a commutative, unitary ring with any ideal $I$. There is utility in pulling out the '$[X]$' and treating any quotient of a ring polynomial as a ring polynomial with coefficients that are quotients i.e. $R[X]/I\cong (R/I)[X]$. Note I'm aware $R[X]/I[X] \cong (R/I)[X]$ holds.

Answer 1

Theorem For a ring $R$ and an element $r \in R$, $R/rR[x] \cong R[x] / r R[x]$.

That $r$ is irreducible is an unnecessary assumption.

You gave one map $R[x] \rightarrow R/rR [x]$. For a map going the other way, take $R \rightarrow R[x] \rightarrow R[x] / rR[x]$. This kills $rR$, and so factors through $R/rR$ by a map $R/rR \rightarrow R[x] / rR[x]$. There is a canonical map $R/rR[x] \rightarrow R[x] / rR[x]$ sending $x$ to $\overline{x}$. The resulting map sends $\sum_{i = 1}^n \overline{a_i} x^i$ to $\overline{\sum_{i = 1}^n a_i x_i}$.

Now one must show these two maps are inverse. But the map you constructed sends $\overline{\sum_{i = 1}^n a_i x_i }$ to $\sum_{i = 1}^n \overline{a_i} x^i$, so that these maps are inverse is immediate.