A complete normal surface resolution converts to normalized point blowups

Given: A complete equicharacteristic normal local surface domain $A$ admitting a proper birational regular model $Z\to \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)

cor-complete-local-domain-finite-over-a-regular-power-series-ring. Assume the Axiom of Choice. Let $(A,\mathfrak{m})$ be a complete equicharacteristic Noetherian local domain of dimension $d$. Then there exists a coefficient field $k\subseteq A$ and an injective local homomorphism $k\mathrm{⟦}{X}_1,\dots ,X_d\mathrm{⟧}\hookrightarrow A$ whose image is a regular complete local subring over which $A$ is module-finite. (A complete local domain is finite over a regular power-series ring)

lem-normalized-point-blowups-dominate-local-normal-surface-modifications. Assume AC and DC. Let $A$ be a normal two-dimensional Noetherian local domain essentially of finite type over a field or a complete equicharacteristic Noetherian local ring. Let $S$ be a normal integral modification of $\mathrm{Spec}A$, and let $Y\to S$ be an integral modification with normal $Y$. (Normalized point blowups dominate local normal surface modifications)

lem-local-normal-surface-modification-dimension-and-projective-cohomology. Assume AC and DC. Let $(A,\mathfrak{m})$ be a normal Noetherian local domain of dimension two and $f:X\to \mathrm{Spec}A$ an integral modification. Then $X$ has dimension two, all closed points have local dimension two, $f$ is an isomorphism off the closed point, $f_{\ast }{\mathcal{O}}_X={\mathcal{O}}_{\mathrm{Spec}A}$, and its special fibre has dimension at most one. (Dimension and cohomology of local normal surface modifications)

lem-surface-open-regular-locus. Assume AC and DC. Every finite-type algebra over a field or a complete equicharacteristic Noetherian local ring has open regular locus. Thus the regular locus of any scheme locally of finite type over one of these bases is open. (Surface open regular locus)

lem-proper-source-to-separated-target-proper. Assume the Axiom of Choice. Let $f:X\to S$ be proper and let $g:Y\to S$ be separated. Then every $S$-morphism $h:X\to Y$ is proper. No Noetherian, reducedness or nonemptiness hypothesis is used, and the empty source is included. (Morphisms from a proper scheme to a separated one are proper)

lem-regular-local-surface-is-rational-by-point-blowup-domination. Assume AC and DC. A regular two-dimensional local domain in the permitted finite-type class defines a rational singularity. (Regular local surfaces have rational modification cohomology)

lem-rational-surface-local-rings-propagate-by-point-sequence-spreading. Assume AC and DC. If a permitted normal local surface domain $A$ is rational and $A\subset B$ is a normal two-dimensional local domain with the same fraction field, essentially of finite type over $A$, then $B$ is rational. (Rationality propagates to birational local surface rings)

lem-normal-projective-surface-dualizing-module-over-regular-local-base. Assume AC and DC. Let $R$ be a regular Noetherian local ring of dimension two, let $A$ be a finite normal local $R$-domain of dimension two, with $R\hookrightarrow A$ local, and let $X$ be a normal integral scheme of dimension two projective over $R$, with a proper birational map $f:X\to \mathrm{Spec}A$. Put ${\omega }_A={\mathrm{Hom}}_R(A,R)$. (Dualizing modules and trace pairing for normal projective surface modifications)

lem-rational-normal-surface-reduced-to-invertible-canonical-module. Assume AC and DC. A rational normal local surface domain in the permitted regular-base dualizing setting admits a finite sequence of ordinary point blowups at singular closed points, with each model normal and projective, whose terminal canonical module is invertible. (Rational normal surfaces reduce to an invertible canonical module)

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-rational-gorenstein-normal-surface-singularity-resolved-by-point-blowups. Assume AC and DC. A rational Gorenstein normal local surface domain in the permitted canonical-module setting with normal completion is resolved by finitely many ordinary blowups at singular closed points. Every model is normal, its closed local rings are rational, and its canonical module is invertible; the terminal model is regular and projective over the local base. (Rational Gorenstein normal surface singularities resolve by point blowups)

lem-local-normalized-point-blowup-sequences-spread-at-closed-points. Assume AC and DC. Let $X$ be a normal integral surface locally of finite type over a permitted base and $x\in X$ a closed point with two-dimensional local ring $B$. Any finite normalized point-blowup sequence over $\mathrm{Spec}B$ spreads to the same finite sequence of normalized blowups at closed points of $X$, unchanged off $x$. (Local normalized point sequences spread at closed surface points)

lem-blowup-of-closed-point-of-regular-surface-is-regular. Assume the Axiom of Choice (The Axiom of Choice). Let $S$ be a regular surface: a locally Noetherian scheme of pure dimension two all of whose local rings are regular (def-embedding-dimension-and-regular-local-ring). (Point blowups of regular surfaces stay regular, with rational exceptional curves at two-dimensional local rings)