Normalization of a surface modification commutes with local-base completion

Given: A normal local surface domain $A$ essentially of finite type over a field or a complete equicharacteristic local base, with normal completion $\widehat{A}$, and an integral modification $X$ of $\mathrm{Spec}A$.

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-dependent-choice. Let $X$ be a set and let $R\subseteq X\times X$ be a binary relation on $X$. Call $R$ entire on $X$ when $\text{for every }x\in X\text{ there is }y\in X\text{ with }xRy\mathrm{.}$ The Axiom of Dependent Choice, written $\mathrm{D}\mathrm{C}$, is the following statement. (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain)

def-normal-surface-modification-and-normalized-point-blowup. Normal schemes. A locally Noetherian scheme is normal if every local ring ${\mathcal{O}}_{X,x}$ is an integrally closed domain (def-normal-noetherian-ring). This is a local condition on the local rings and is checked on an affine open cover; it does not require the global section ring to be a domain. The empty scheme is normal vacuously. (Normal scheme modifications and normalized point blowups)

lem-surface-finite-type-formal-fibres. Assume AC and DC. Let $A$ be a field or a complete equicharacteristic Noetherian local ring and $B$ an essentially finite-type $A$-algebra. Every formal fibre of every local ring of $B$ is geometrically regular over its residue fraction field. (Surface finite type formal fibres)

lem-surface-finite-type-normalization-finite. Assume AC and DC. Every integral finite-type algebra over a field or a complete equicharacteristic Noetherian local base has finite normalization, and so do its localizations. Integral schemes of finite type over these bases consequently have finite scheme normalization. (Surface finite type normalization finite)

lem-surface-regular-fibres-preserve-normality. Assume AC and DC. A flat map of Noetherian rings with regular fibres carries normality of the base to normality of the target. Consequently a normal essentially finite-type local ring over a field or complete equicharacteristic Noetherian local base has normal maximal-adic completion, which is a domain. (Surface regular fibres preserve normality)

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-integrality-commutes-with-localisation. Let $A\to B$ be a homomorphism of commutative rings, let $S\subseteq A$ be multiplicative, and let $b\in B$. 1. If $b$ is integral over $A$, then $b\mathrm{/}1$ is integral over $S^{-1}A$ in $S^{-1}B$. 2. If $b\mathrm{/}1$ is integral over $S^{-1}A$ in $S^{-1}B$, then some $s\in S$ makes $sb$ integral over $A$. (Integrality and integral closure commute with localisation)