Normalized point sequences and resolutions descend from completion

Given: A normal local surface domain $A$ as in the normalization-completion lemma and a finite sequence of normalized point blowups over $\mathrm{Spec}\widehat{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)

lem-normal-surface-normalization-commutes-with-base-completion. Assume AC and DC. Let $A$ be a normal local surface domain essentially of finite type over a field or a complete equicharacteristic local base, with normal completion $\widehat{A}$. (Normalization of a surface modification commutes with local-base completion)

lem-proper-surface-regularity-transfers-to-and-from-completion. Assume AC. Let $(A,\mathfrak{m})$ be a Noetherian local ring and $X\to \mathrm{Spec}A$ locally of finite type. Set $Y=X{\times }_A\widehat{A}$. For $y\in Y$ with image $x\in X$, regularity of ${\mathcal{O}}_{Y,y}$ implies regularity of ${\mathcal{O}}_{X,x}$. If $y$ lies on the closed fibre, the two local rings are regular simultaneously. (Regularity of a proper scheme transfers to and from local-base completion)

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)

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)

thm-blowup-base-change-flat. Assume the Axiom of Choice as inherited from the relative Proj construction. Let $g\text{\hspace{0.17em}⁣}:X^{\mathrm{\prime }}\to X$ be a flat morphism of schemes and $\mathcal{I}$ a quasi-coherent ideal sheaf of finite type on $X$. (Flat base change for blowups, and failure without flatness)