completion preserves embedding dimension

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

embedding dimension and regular local ring: For a nonzero commutative Noetherian local ring $(R,\mathfrak{m},k)$, define $\mathrm{edim}R={\dim }_k(\mathfrak{m}\mathrm{/}{\mathfrak{m}}^2)$. The ring is regular local when $\mathrm{edim}R=\dim R$. The cotangent space is intrinsic, and is finite-dimensional because $\mathfrak{m}$ is finitely generated.

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 commutes with finite quotients and induced submodules: Assume the Axiom of Choice. Let $R$ be a Noetherian commutative ring, let $I\subseteq R$ be an ideal, and let $N\subseteq M$ be finitely generated $R$-modules. 1. The natural map $\widehat{M}\mathrm{/}\widehat{N}⟶\widehat{M\mathrm{/}N}$ is an isomorphism. 2. Under the natural map $\widehat{N}\to \widehat{M}$, the image of $\widehat{N}$ is the $\widehat{R}$-submodule $N\widehat{R}\subseteq \widehat{M}$. In particular, for every ideal $J\subseteq R$, $\widehat{JM}\cong J\widehat{M}\mathrm{.}$ 3. For every $n\ge 0$, $\widehat{M}\mathrm{/}{I}^n\widehat{M}\cong M\mathrm{/}{I}^{n}M\mathrm{.}$