Resolution of normal surface singularities

Given: A field $k$ of arbitrary characteristic and a normal integral scheme $Y$ of finite type over $k$ 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)

thm-complete-equicharacteristic-normal-surface-resolution-by-normalized-point-blowups. Assume AC and DC. Every complete equicharacteristic Noetherian normal local domain $A$ of dimension two admits a regular resolution by finitely many normalized point blowups at singular closed points. All normalizations are finite and the resulting morphism is projective, birational, and an isomorphism off the original closed point. (Complete equicharacteristic normal surfaces resolve by normalized point blowups)

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-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}$. (lem-normal-surface-normalization-commutes-with-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-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-normal-finite-type-surface-resolution-globalizes-from-complete-local-points. Assume AC and DC. Let $Y$ be a normal integral finite-type surface over any field. If each completed local ring at a singular closed point has a regular resolution by finitely many normalized point blowups at singular centres, then $Y$ has such a finite global sequence, proper and birational over $Y$ and an isomorphism on the regular locus. (Surface resolution globalizes from complete local point resolutions)

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-regular-equals-smooth-over-perfect-field. Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be a perfect field and let $X$ be a finite-type $k$-scheme. Here regular means that $X$ is locally Noetherian and every local ring ${\mathcal{O}}_{X,x}$ is regular local; smooth over $k$ means that $X\to \mathrm{Spec}k$ is smooth under the classical local-standard-smooth convention. (Regular equals smooth over a perfect field)

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

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)

def-birational-morphism-schemes. Let $k$ be a field and let $X$ and $Y$ be integral $k$-schemes of finite type (def-integral-scheme, def-locally-finite-type-and-finite-type-morphism). (Birational morphisms of integral finite-type schemes)

thm-stalk-structure-sheaf-prime-localization. For $\mathfrak{p}\in \mathrm{Spec}A$, there is a canonical isomorphism ${\mathcal{O}}_{\mathrm{Spec}A,\mathfrak{p}}\cong A_{\mathfrak{p}}$. (The stalk of the affine structure sheaf at a prime is A_p)