Regular local rings are domains

Remarks

Proof idea: let $d = \dim R$ and $k = R/\mathfrak m$. A regular system of parameters $x_1, \ldots, x_d$ gives a surjection $k[X_1, \ldots, X_d] \to \operatorname{gr}_{\mathfrak m} R = \bigoplus_n \mathfrak m^n / \mathfrak m^{n+1}$ onto the associated graded ring. Comparing dimensions shows that this surjection is an isomorphism, so $\operatorname{gr}_{\mathfrak m} R$ is a polynomial ring, hence a domain. By the Krull intersection theorem, $\bigcap_n \mathfrak m^n = 0$, so each nonzero $a \in R$ has an order $n$ with $a \in \mathfrak m^n \setminus \mathfrak m^{n+1}$. The leading forms of two nonzero elements multiply to a nonzero form, so their product is nonzero.

Example: $k[\![x, y]\!]$ and $\Z_{(p)}[x]_{(p, x)}$ are regular local rings, hence domains.

The hypothesis $\dim R = \operatorname{edim} R$ cannot be dropped. The Noetherian local ring $R = k[x, y]_{(x, y)}/(xy)$ has dimension $1$ and embedding dimension $2$, and it is not a domain, since $x \cdot y = 0$ with $x, y \ne 0$.

Going deeper

For a student

The statement is the first step in the theory of regular local rings. The stronger theorem that regular local rings are UFDs uses it together with homological tools such as Serre's theorem on regular local rings. It also implies that a regular local ring of dimension $1$ is a discrete valuation ring.