LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Fibres of a proper birational morphism of regular surfaces

Statement

Assume the Axiom of Choice. Let $k$ be a field, let $X$ and $Y$ be integral regular finite-type $k$ -schemes of pure dimension two, let $f ⁣ : X \to Y$ be a proper birational morphism and let $y \in Y$ be a closed point. Put $F = f^{- 1} (y)$ . Then:

$F$ is a proper $κ (y)$ -scheme with $\dim F \leq 1$ .
If $\dim F = 1$ , then $F$ has finitely many irreducible components $C_{1}, \dots, C_{r}$ ; each, with its reduced induced structure, is an integral proper curve over $κ (y)$ (Integral schemes, Fibres of proper morphisms are proper); and each $C_{i}$ contains a closed point $x_{i}$ with $x_{i} \notin C_{j}$ for every $j \neq i$ .
For every generic point $ξ$ of a one-dimensional component of $F$ the local ring $O_{X, ξ}$ is a discrete valuation ring, and $f^{♯}$ identifies the function field of $Y$ with the function field of $X$ .
The set $N (f)$ of integral curves $C \subseteq X$ with $\dim f (C) = 0$ is finite. More precisely, the non-étale locus $Z \subseteq X$ of $f$ (The étale locus of a morphism) is closed and not all of $X$ , every contracted curve is contained in $Z$ , and $N (f)$ is at most the number of irreducible components of $Z$ .
If $f$ is not an isomorphism, then $N (f) > 0$ . Equivalently, if every fibre of $f$ is finite, then $f$ is an isomorphism.

Facts & Assumptions

Given: A field $k$ , integral regular finite-type $k$ -schemes $X$ and $Y$ of pure dimension two, a proper birational morphism $f ⁣ : X \to Y$ and a closed point $y \in Y$ .

[F1]

lem-proper-fibres-proper. Assume the Axiom of Choice. Let $f : X \to S$ be a proper morphism of schemes and let $s \in S$ be a point, not necessarily closed. Then the scheme-theoretic fibre $X_{s} = X \times_{S} Spec κ (s)$ is proper over $Spec κ (s)$ . (Fibres of proper morphisms are proper)

[F2]

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

[F3]

def-dimension-noetherian-topological-space. For a Noetherian topological space $T$ , define $\dim T$ as the supremum of the lengths $s$ of strict chains $Z_{0} ⊊ \dots ⊊ Z_{s}$ of nonempty irreducible closed subsets of $T$ . Thus a one-member chain has length zero. Set $\dim \emptyset = - \infty$ , and allow $\dim T = + \infty$ . The supremum of an empty family of dimensions is $- \infty$ . (Chain dimension and the empty-space convention)

[F4]

def-locally-noetherian-and-noetherian-scheme. A scheme is locally Noetherian if it has an affine open cover by spectra of Noetherian rings. It is Noetherian if it is locally Noetherian and quasi-compact; equivalently, it has a finite affine open cover by spectra of Noetherian rings. (Locally Noetherian and Noetherian schemes)

[F5]

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)

[F6]

def-embedding-dimension-and-regular-local-ring. For a nonzero commutative Noetherian local ring $(R, m, k)$ , define $edim R = \dim_{k} (m / m^{2})$ . The ring is regular local when $edim R = \dim R$ . The cotangent space is intrinsic, and is finite-dimensional because $m$ is finitely generated. (embedding dimension and regular local ring)

[F7]

def-etale-locus-morphism. Let $f : X \to S$ be a morphism locally of finite presentation (def-locally-finite-presentation-morphism). The étale locus of $f$ is $Et (f) = {x \in X : the morphism f is \overset{ˊ}{e} tale at x} \subseteq X,$ the set of points at which the conditions of def-etale-morphism-schemes hold. (The étale locus of a morphism)

[F8]

thm-etale-locus-open. Assume the Axiom of Choice (The Axiom of Choice). Let $f ⁣ : X \to S$ be a morphism locally of finite presentation (def-locally-finite-presentation-morphism) and let $Et (f) = {x \in X : f is \overset{ˊ}{e} tale at x}$ be its 'etale locus (The étale locus of a morphism). (The etale locus is open)

[F9]

thm-etale-morphisms-open-and-quasi-finite. Assume the Axiom of Choice (The Axiom of Choice). Let $f ⁣ : X \to S$ be 'etale (def-etale-morphism-schemes). 1. $f$ is flat and locally of finite presentation (def-flat-morphism-schemes, def-locally-finite-presentation-morphism) and therefore universally open (def-open-morphism-schemes). 2. (Etale morphisms are universally open and quasi-finite at every point)

[F10]

def-quasi-finite-morphism-schemes. A morphism of schemes $f : X \to S$ is quasi-finite if it is of finite type (def-locally-finite-type-and-finite-type-morphism) and, for every point $x \in X$ , there are affine neighbourhoods $U = Spec (B)$ of $x$ and $V = Spec (A)$ of $f (x)$ such that $f (U) \subseteq V$ and the induced finite-type ring map $A \to B$ is quasi-finite at the prime (Quasi-finite morphisms of schemes)

[F11]

thm-proper-quasi-finite-is-finite. Assume the Axiom of Choice. Every proper quasi-finite morphism of schemes $f : X \to S$ is finite (Proper morphisms, Quasi-finite morphisms of 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)

[F18]

thm-normality-is-local-for-domains. Assume AC. For a domain $A$ , integrally closedness is equivalent to integral closedness of every maximal localization $A_{m}$ . Thus a regular Noetherian domain whose local rings are regular local is integrally closed, since the local criterion applies to its maximal localizations. (A domain is integrally closed if and only if its prime localisations are, equivalently if and only if its maximal localisations are)

[F19]

thm-finite-morphism-integral-closed. Assume AC. If $g : Y \to S$ is finite, then on every affine open $U = Spec (A) \subseteq S$ with $g^{- 1} (U) = Spec (B)$ , the ring map $A \to B$ is integral. (Finite morphisms are integral and universally closed)

[F13]

cor-closed-points-dense-in-affine-spectra. Assume the Axiom of Choice. Let $k$ be a field, let $A$ be a finite-type $k$ -algebra, and let $Z \subseteq Spec (A)$ be closed. Then every nonempty open subset of $Z$ contains a closed point of $Spec (A)$ . Equivalently, the closed points are dense in every closed subset of $Spec (A)$ . (In a finite-type algebra over a field, closed points are dense in every closed subset of the spectrum)

[F14]

def-integral-scheme. An integral scheme is a nonempty scheme that is reduced and whose underlying topological space is irreducible. Equivalently, it is nonempty and every nonempty affine open is the spectrum of a domain. The latter criterion is independent of the chosen affine open cover. (Integral schemes)

[F15]

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)

[F16]

thm-regular-local-rings-are-normal. Assume the Axiom of Choice (The Axiom of Choice). Every regular local ring is an integrally closed domain. Every commutative regular Noetherian ring is normal and is a finite product of regular domains, with the zero ring corresponding to the empty product. (regular local rings are normal)

[F17]

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 $F$ all of whose members are nonempty, there exists a function $g$ with domain $F$ satisfying $g (S) \in S$ for all $S \in F$ . (The Axiom of Choice)

[F20]

A quasi-finite finite-type algebra is source-locally a principal localization of a finite subalgebra of its relative integral closure; the quasi-finite locus is open. (Quasi-finite algebras are source locally localizations of finite algebras, The quasi-finite locus of a finite-type algebra is open)

Proof

1.1F1F2F3F4F14

The fibre $F = f^{- 1} (y)$ is a proper $κ (y)$ -scheme by properness of $f$ , and $F$ is closed in $X$ of dimension at most one: a closed irreducible subset of the integral scheme $X$ of the same dimension two would equal $X$ , forcing $f (X) = {y}$ and contradicting dominance of the birational morphism $f$ .

2.1F1F4F13F14F15F16F18F20step 1.1

Assume $\dim F = 1$ ; there can be no isolated zero-dimensional component. Indeed at an isolated fibre point $x$ , the morphism is quasi-finite. On affine normal target and quasi-finite source neighbourhoods, the source-local finite-algebra factorization gives a principal open immersion: its finite intermediate algebra lies in the common fraction field and is integral over the normal target, hence equals that target. Its inverse is a section over a target open; the section is closed because $f$ is separated, and its image contains the generic point of the integral inverse image, so it is the whole inverse image (the defining ideal is zero by reducedness). Thus the entire fibre would be one point, contrary to $\dim F = 1$ . Now Noetherianity gives finitely many irreducible components $C_{1}, \dots, C_{r}$ , each of dimension one, and each $C_{i}$ with its reduced induced structure is an integral proper curve over $κ (y)$ as a closed subscheme of $F$ . The open subset of $C_{i}$ obtained by removing the finitely many closed sets $C_{j} \cap C_{i}$ , $j \neq i$ , is nonempty because $C_{i}$ is irreducible and no $C_{j}$ contains it; by density of closed points in finite-type $k$ -schemes it contains a closed point $x_{i}$ , which is closed in $F$ and lies on no other $C_{j}$ .

3.1F2F5F6step 2.1

For the generic point $ξ$ of a one-dimensional component of $F$ the local ring $O_{X, ξ}$ is a regular local ring of dimension one, because $X$ is regular of pure dimension two and the closure of $ξ$ has dimension one; by the one-dimensional criterion it is a discrete valuation ring. Since $f$ is birational, the stalk map identifies $K (Y) = O_{Y, η_{Y}}$ with $O_{X, η_{X}} = K (X)$ , and in particular $f^{♯}$ is injective on the function field of $Y$ .

4.1F7F9F10step 3.1

Let $C \subseteq X$ be an integral curve with $f (C)$ a single point and let $ξ$ be its generic point. The fibre of $f$ through $ξ$ contains $C$ , so $f$ is not quasi-finite at $ξ$ ; since an etale morphism is quasi-finite at every point, $f$ is not etale at $ξ$ . Hence $ξ \notin Et (f)$ , and since the non-etale locus $Z = X ∖ Et (f)$ is closed, $C \subseteq Z$ .

5.1F2F7F8step 4.1

The non-etale locus $Z$ is closed because $Et (f)$ is open, and $Z \neq X$ : the generic point $η_{X}$ of the integral scheme $X$ lies in $Et (f)$ , since the stalk map $K (Y) \to K (X)$ is an isomorphism of fields, hence flat with trivial residue field extension.

6.1F3F4step 4.1step 5.1

Every component of $Z$ has dimension at most one: a closed component of dimension two would equal $X$ , contradicting step 5.1. If $C$ is a contracted integral curve contained in $Z$ and $Z_{0}$ is a component of $Z$ containing $C$ , then $\dim Z_{0} = 1$ and $C \subseteq Z_{0}$ are irreducible closed subsets of $X$ of dimension one, so $C = Z_{0}$ ; distinct contracted curves therefore lie in distinct components of $Z$ , and the set $N (f)$ has at most as many elements as $Z$ has components, a finite number because $X$ is Noetherian.

7.1F2F11F15F16F18F19step 6.1

If every fibre of $f$ is finite then $f$ is quasi-finite, hence finite because it is proper. Cover $Y$ by affine opens $U = Spec (A)$ ; their inverse images are affine $f^{- 1} (U) = Spec (B)$ and $A \to B$ is integral by [F19]. Both are domains, and birationality identifies their fraction fields and makes $A \to B$ injective. Every maximal localization of $A$ is a regular local ring, hence integrally closed by [F16]; [F18] then implies that $A$ is integrally closed. Since $B$ lies in the common fraction field and is integral over $A$ , $B \subseteq A$ , so $A = B$ on every such chart. Therefore $f$ is an isomorphism.

8.1F3F14step 2.1step 7.1F17∎

Conversely, if $N (f)$ is empty then every fibre of $f$ is finite: a fibre containing a one-dimensional irreducible component would contain the generic point of an integral curve contracted by $f$ , giving an element of $N (f)$ . Together with the previous step this shows that $f$ is an isomorphism if and only if $N (f)$ is empty.

Remarks

The conclusion $\dim F \leq 1$ is the only place where birationality enters as dominance; all remaining arguments use properness, regularity and normality.
The non-etale locus $Z$ is the scheme-theoretically meaningful carrier of the contracted curves; the count in assertion 4 is by components, not by points of $Z$ .

Depends on

Used by

Dependency tree · two levels

97 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

The Stacks Project, Resolution of Surfaces, Section 54.7 (Vanishing) (standard reference, not scraped)
The Stacks Project, Resolution of Surfaces, Chapter 54 (complete chapter PDF) (standard reference, not scraped)