Complete equicharacteristic normal surfaces resolve by normalized point blowups

Given: A complete equicharacteristic Noetherian normal local domain $A$ of dimension two.

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-surface-finite-completion-factors. Assume AC. For a finite map $R\to S$ of Noetherian rings and $\mathfrak{p}\in \mathrm{Spec}R$, $\widehat{R_{\mathfrak{p}}}{\otimes }_{R}S\cong {\prod }_{\mathfrak{q}\cap R=\mathfrak{p}}\widehat{S_{\mathfrak{q}}}$. The finitely many factors use their maximal-adic completions. Thus formal fibres for finite extensions are factors of residue-field base changes of the original formal fibres. (Surface finite completion factors)

lem-finite-normal-surface-cover-completed-local-degree-bound. Assume AC and DC. Let $X\to Y$ be finite dominant of degree $n$ between integral normal surfaces in the permitted class, with $Y$ regular. At a closed $x\in X$ over a point $y\in Y$ with $\dim O_{Y,y}=2$, the complete normal local domain $\widehat{O_{X,x}}$ is finite over the complete regular local ring $\widehat{O_{Y,y}}$, and its fraction-field degree is at most $n$. (Completed local degrees of finite normal surface covers)

lem-normalized-surface-point-blowup-resolution-descends-from-completion. Assume AC and DC. For $A$ as in the preceding normalization-completion lemma, every finite sequence of normalized point blowups over $\mathrm{Spec}\widehat{A}$ has a uniquely corresponding finite sequence over $\mathrm{Spec}A$ with isomorphic base-changed models. Each centre lies over the closed point. (Normalized point sequences and resolutions descend from completion)

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-complete-normal-surface-regular-resolution-converts-to-normalized-point-blowups. Assume AC and DC. If a complete equicharacteristic normal local surface domain $A$ admits a proper birational regular model, then it admits a regular terminal model obtained by finitely many normalized point blowups. The centres can all be chosen singular; the normalizations are finite. (A complete normal surface resolution converts to normalized point blowups)

lem-complete-regular-surface-degree-p-extension-has-bounded-h1. Assume AC and DC. Let $A=k[\text{\hspace{0.17em}⁣}[u,v]\text{\hspace{0.17em}⁣}]$ have characteristic $p>0$, let $L\mathrm{/}K$ be a purely inseparable degree-$p$ extension of its fraction field, and let $B$ be the finite normalization of $A$ in $L$. Then normal modification H1 over $B$ is uniformly bounded. (Degree-p inseparable extensions of complete regular surfaces have bounded H1)

lem-finite-separable-normal-surface-extension-preserves-bounded-h1. Assume AC and DC. Let $A\subset B$ be a finite injective local extension of permitted normal local surface domains with separable fraction-field extension. If modification H1 over $A$ is uniformly bounded, so is modification H1 over $B$. (Separable finite surface extensions preserve bounded 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. If modification $H^1$ over $A$ is uniformly bounded, a finite normalized point-blowup sequence has rational local rings at every closed point of its terminal surface. (Rationality propagates to birational local surface rings)

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)

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-surface-complete-equicharacteristic-finite-integral-closure. Assume AC. The integral closure of a complete equicharacteristic Noetherian local domain in every finite extension of its fraction field is a finite module. (Surface complete equicharacteristic finite integral closure)

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-finite-over-projective-noetherian-affine-base-is-projective. Assume AC. Let $R$ be Noetherian, let $X$ be projective over $R$, and let $Y\to X$ be finite. Then $Y\to X$ admits a closed immersion into one relative projective space over $X$, and $Y$ is projective over $R$. Finite compositions of projective morphisms between such schemes are projective. (Finite schemes over projective schemes are projective over a Noetherian affine base)

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-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)

A normal essentially finite-type local ring over a field or complete equicharacteristic Noetherian local base has normal maximal-adic completion, a domain. (Surface regular fibres preserve normality)