A normal-surface modification is an isomorphism in codimension one

Given: A modification $f\text{\hspace{0.17em}⁣}:X\to S$ of integral Noetherian schemes with $S$ normal of dimension two.

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)

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)

lem-normal-domain-implies-r-one. Every commutative Noetherian integrally closed domain satisfies $(R_1)$. (normal domain implies r one)

thm-one-dimensional-regular-local-rings-are-dvrs. Assume the Axiom of Choice (The Axiom of Choice). A nonzero Noetherian local ring of dimension one is regular if and only if it is a discrete valuation ring. Fields are excluded from the term DVR. (one dimensional regular local rings are dvrs)

thm-valuative-criterion-properness. Assume the Axiom of Choice. Let $f:X\to S$ be a morphism of schemes that is of finite type and quasi-separated. Then $f$ is proper if and only if every valuative diagram for $f$ over an arbitrary valuation ring has exactly one lift. (Valuative criterion for properness)

cor-quasi-finite-locus-open-finite-type-algebra. Assume the Axiom of Choice (The Axiom of Choice). Let $R\to S$ be a ring map of finite type (def-finite-type-and-module-finite-algebras). (The quasi-finite locus of a finite-type algebra is open)

thm-proper-quasi-finite-is-finite. Assume the Axiom of Choice. Every proper quasi-finite morphism of schemes $f:X\to S$ is finite (def-proper-morphism, def-quasi-finite-morphism-schemes, def-finite-morphism-schemes). No Noetherian or nonemptiness hypothesis is imposed, and the assertion is local on the base. (A proper quasi-finite morphism is finite)

thm-integrality-and-finite-module-equivalences. Let $A\subseteq B$ be commutative rings with $A\mathrm{\ne }0$, and let $b\in B$. The following are equivalent: $b$ is integral over $A$; $A[b]$ is finitely generated as an $A$-module; and there exists a faithful $A[b]$-module that is finitely generated over $A$, where faithful means that $rM=0$ implies $r=0$ for $r\in A[b]$. See def-integral-element-and-algebraic-integer. (Integrality and finite-module characterizations for one element)

lem-proper-stable-base-change. Assume the Axiom of Choice (AC). For every proper morphism $f:X\to S$ and every morphism $S^{\mathrm{\prime }}\to S$, the base-changed morphism $f_{S^{\mathrm{\prime }}}:X{\times }_S{S}^{\mathrm{\prime }}⟶S^{\mathrm{\prime }}$ is proper. (Properness survives arbitrary base change)

thm-proper-morphism-closed-image. Let $f:X\to S$ be a proper morphism of schemes. Then $f$ is a closed map of topological spaces: for every closed subset $Z\subseteq \mathrm{\mid }X\mathrm{\mid }$ its image $f(Z)$ is closed in $\mathrm{\mid }S\mathrm{\mid }$. In particular $f(X)$ is closed. (Proper morphisms are closed)