Surface resolution globalizes from complete local point resolutions

Given: A normal integral finite-type surface $Y$ over a field, such that each completed local ring at a singular closed point has a regular resolution by finitely many normalized point blowups at singular centres.

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-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-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-normal-domain-implies-r-one. Every commutative Noetherian integrally closed domain satisfies $(R_1)$. (normal domain implies r one)

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-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-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-blowup-projective. Assume the Axiom of Choice, inherited from the relative Proj construction (The Axiom of Choice). Let $X$ be a scheme, let $\mathcal{I}$ be a quasi-coherent ideal sheaf of finite type on $X$ (def-quasi-coherent-ideal-sheaf) and let $\pi \text{\hspace{0.17em}⁣}:{\mathrm{Bl}}_{\mathcal{I}}X\to X$ be the blowup of def-blowup-scheme-along-ideal. Then: 1. (Blowups of finite type ideals are locally H-projective, and proper)