Regularity of a proper scheme transfers to and from local-base completion

Given: A Noetherian local ring $(A,\mathfrak{m})$, a scheme $X\to \mathrm{Spec}A$ locally of finite type, and the base change $Y=X{\times }_{\mathrm{Spec}A}\mathrm{Spec}\widehat{A}$, with $y\in Y$ and image $x\in X$.

def-axiom-of-choice. The Axiom of Choice (AC) is the following statement. > Every family of nonempty sets has a choice function > (def-choice-function). Written out: for every set $\mathcal{F}$ all of whose members are nonempty, there exists a function $g$ with domain $\mathcal{F}$ satisfying $g(S)\in S$ for all $S\in \mathcal{F}$. (The Axiom of Choice)

def-proper-morphism. A morphism of schemes $f:X\to S$ is proper if and only if it is separated, of finite type, and universally closed. Here separatedness has the meaning of def-separated-morphism-schemes, finite type has the meaning of def-locally-finite-type-and-finite-type-morphism, and universally closed has the meaning of def-universally-closed-morphism. (Proper morphisms)

lem-ag-flat-local-regularity-ascent-descent. Assume the Axiom of Choice (The Axiom of Choice). Let $(R,\mathfrak{m})\to (S,\mathfrak{n})$ be a flat local homomorphism (def-flat-and-faithfully-flat-modules-and-ring-maps) of Noetherian local rings, so that $S\mathrm{/}\mathfrak{m}S$ is again a Noetherian local ring. Then: 1. (Regularity ascends and descends along a flat local homomorphism)

lem-proper-stable-base-change. Assume the Axiom of Choice (AC). For every proper morphism $f:X\to S$ and every morphism $S^{\mathrm{\prime }}\to S$, the base-changed morphism $f_{S^{\mathrm{\prime }}}:X{\times }_S{S}^{\mathrm{\prime }}⟶S^{\mathrm{\prime }}$ is proper. (Properness survives arbitrary base change)

thm-completion-of-a-noetherian-local-ring. 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 of a Noetherian local ring is local with the same residue field)

thm-completion-preserves-regular-local-rings. Assume the Axiom of Choice (The Axiom of Choice). A nonzero Noetherian local ring $R$ is regular if and only if its maximal-adic completion $\widehat{R}$ is regular. (completion preserves regular local rings)

cor-localisations-of-regular-local-rings-are-regular. Assume the Axiom of Choice (The Axiom of Choice). Every prime localization $R_{\mathfrak{p}}$ of a regular local ring $R$ is regular, and $\mathrm{edim}{R}_{\mathfrak{p}}=\mathrm{ht}\mathfrak{p}$. (localisations of regular local rings are regular)

lem-surface-completion-base-change-preserves-closed-fibre-local-completions. Assume AC. Let $(A,\mathfrak{m})$ be a Noetherian local ring, $\widehat{A}$ its maximal-adic completion, and $X$ a scheme locally of finite type over $A$. Put $Y=X{\times }_{\mathrm{Spec}A}\mathrm{Spec}\widehat{A}$. The closed fibres of $X$ and $Y$ are canonically isomorphic. (Completion base change preserves completed local rings on the closed fibre)