formal power series ring regular

Given: The objects and hypotheses in the example. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.

localisation and polynomial extension of regular rings: Localizations and finite polynomial extensions of a commutative regular Noetherian ring are regular. Regularity can equivalently be tested at maximal ideals. For every nonzero such ring, $\mathrm{gldim}R=\dim R$, allowing infinity. More generally, for a finite module over any commutative Noetherian ring, projective dimension is the supremum of its prime-local projective dimensions. Dedekind domains and their finite polynomial extensions are regular.

completion preserves regular local rings: A nonzero Noetherian local ring $R$ is regular if and only if its maximal-adic completion $\widehat{R}$ is regular.

completion preserves embedding dimension: For a nonzero Noetherian local ring $(R,\mathfrak{m},k)$, its maximal-adic completion $\widehat{R}$ has maximal ideal $\widehat{\mathfrak{m}}=\mathfrak{m}\widehat{R}$, residue field $k$, and a canonical isomorphism $\mathfrak{m}\mathrm{/}{\mathfrak{m}}^2\cong \widehat{\mathfrak{m}}\mathrm{/}{\widehat{\mathfrak{m}}}^2$. In particular their embedding dimensions agree.

Completion of a Noetherian local ring is local with the same residue field: Assume the Axiom of Choice. Let $(R,\mathfrak{m})$ be a Noetherian local ring, and let $\widehat{R}$ be its $\mathfrak{m}$-adic completion. 1. $\widehat{R}$ is a Noetherian local ring with maximal ideal $\mathfrak{m}\widehat{R}$. 2. The residue field is unchanged: $\widehat{R}\mathrm{/}\mathfrak{m}\widehat{R}\cong R\mathrm{/}\mathfrak{m}\mathrm{.}$ 3. The completion map $R\to \widehat{R}$ is faithfully flat.

Completion preserves dimension and Hilbert-Samuel data: Assume the Axiom of Choice. Let $(R,\mathfrak{m})$ be a Noetherian local ring, let $M\mathrm{\ne }0$ be a finitely generated $R$-module, and let $\widehat{R}$, $\widehat{M}$ denote the $\mathfrak{m}$-adic completions. 1. For every $n\ge 0$, $\widehat{M}\mathrm{/}{\mathfrak{m}}^{n+1}\widehat{M}\cong M\mathrm{/}{\mathfrak{m}}^{n+1}M\mathrm{.}$ In particular the Hilbert-Samuel functions of $M$ and $\widehat{M}$ agree. 2. The Hilbert-Samuel multiplicity of $M$ equals that of $\widehat{M}$. 3. The support dimensions of $M$ and $\widehat{M}$ are equal.

dimension at most embedding dimension: Every nonzero commutative Noetherian local ring $R$ satisfies $\dim R\le \mathrm{edim}R<\mathrm{\infty }$.