Grauert–Riemenschneider vanishing for the required normal surface modifications

Given: A regular Noetherian local ring $R$ of dimension two, a finite normal local $R$-domain $A$ of dimension two with $R\hookrightarrow A$ local, a projective normal modification $X\to \mathrm{Spec}A$ in the permitted class, and ${\omega }_A={\mathrm{Hom}}_R(A,R)$ with normalized dualizing module ${\omega }_X$.

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)

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

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-normal-surface-modification-no-derived-residue-map. Assume AC and DC. For $A,X$ as in the preceding injection lemma, with residue field $\kappa$, ${\mathrm{Hom}}_{D(A)}(\kappa [-1],R\mathrm{\Gamma }(X,{\mathcal{O}}_X))=0$. (No derived residue map into structure cohomology of a normal surface modification)

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-finite-length-duality-over-a-regular-local-base. Assume AC and DC. Let $(R,\mathfrak{m})$ be regular Noetherian local of dimension $d$ and let $(B,\mathfrak{n})$ be a module-finite local $R$-algebra with the map local. For finite-length $B$-modules put $T(M)={\mathrm{Ext}}_R^d(M,R)$ with its natural $B$-action. (Finite-length duality over a regular local base)

lem-finite-regular-base-algebra-dualizing-biduality. Assume AC and DC. Let $R$ be a regular Noetherian ring of finite dimension $d$, and let $B\mathrm{\ne }0$ be a module-finite $R$-algebra. For any integer $s$, $D_B=R{\mathrm{Hom}}_R(B,R[s])$ is a dualizing complex over $B$. (Dualizing biduality for finite algebras over a regular base)

thm-proper-pushforward-coherent. Assume the Axiom of Choice and the Axiom of Dependent Choice, inherited from the affine localization theorem, the Čech comparison and the dévissage lemma cited below (The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). (Coherent higher direct images under proper morphisms)

Finite schemes over a projective scheme with Noetherian affine base are projective, and finite compositions of these projective morphisms are projective. (Finite schemes over projective schemes are projective over a Noetherian affine base)