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.

A birational morphism of regular surfaces factors through the blowup of a point where its inverse is undefined

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 that are proper over $k$ , and let $f ⁣ : X \to Y$ be a birational morphism. Let $y \in Y$ be a closed point at which the inverse rational map $f^{- 1} ⁣ : Y ⇢ X$ is not defined (Rational maps of integral finite-type schemes, Rational maps of integral finite-type schemes). Then $f$ factors through the blowup $b ⁣ : {Bl}_{y} Y \to Y$ : there is a unique $k$ -morphism $g ⁣ : X \to {Bl}_{y} Y$ with $b \circ g = f$ . Equivalently, the ideal $f^{- 1} m_{y} \cdot O_{X}$ is invertible.

Facts & Assumptions

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

[F1]

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)

[F2]

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)

[F3]

def-rational-map-integral-schemes. Let $k$ be a field and let $X$ be an integral $k$ -scheme of finite type and $Y$ a $k$ -scheme of finite type (def-integral-scheme, def-locally-finite-type-and-finite-type-morphism) with $Y$ separated over $k$ (def-separated-morphism-schemes). (Rational maps of integral finite-type schemes)

[F4]

For an integral finite-type $k$ -scheme and a separated finite-type target, a rational map is represented on nonempty opens; a point of indeterminacy is a point at which no representative is defined. (Rational maps of integral finite-type schemes)

[F5]

lem-normalized-point-blowups-dominate-local-normal-surface-modifications. Assume AC and DC. Let $A$ be a normal two-dimensional Noetherian local domain essentially of finite type over a field or a complete equicharacteristic Noetherian local ring. Let $S$ be a normal integral modification of $Spec A$ , and let $Y \to S$ be an integral modification with normal $Y$ . (Normalized point blowups dominate local normal surface modifications)

[F6]

lem-universal-property-of-a-contraction. Assume the Axiom of Choice, inherited from the blowup suppliers. Let $X$ be a Noetherian scheme, $E \subseteq X$ an exceptional curve of the first kind and $b ⁣ : X \to X^{'}$ a contraction of $E$ (def-exceptional-curve-and-contraction). Write $x^{'} = b (E) \in X^{'}$ . Then: 1. (Universal property and uniqueness of a contraction)

[F7]

lem-proper-birational-normal-target-isomorphism-at-quasi-finite-point. Assume AC. Let $f : X \to S$ be a proper birational morphism of integral Noetherian schemes with normal $S$ . If $f$ is quasi-finite at $x \in X$ , then $f$ is an isomorphism over an open neighbourhood of $f (x)$ ; in particular that fibre consists of $x$ . (A proper birational map to a normal target is an isomorphism near a quasi-finite point)

[F8]

thm-blowup-universal-property. Assume the Axiom of Choice. Let $I$ be a quasi-coherent ideal sheaf of finite type on $X$ with zero scheme $Z$ , and let $π ⁣ : {Bl}_{I} X \to X$ be the blowup. For every $X$ -scheme $f ⁣ : Y \to X$ such that the inverse image $f^{- 1} (Z)$ is an effective Cartier divisor on $Y$ , there is a unique $X$ -morphism $Y \to {Bl}_{I} X$ . (Universal property of the blowup)

[F9]

thm-blowup-regular-surface-closed-point-regular. Assume the Axiom of Choice. Let $S$ be a regular finite-type $k$ -scheme of pure dimension two, let $p$ be a closed point, put $κ = κ (p)$ and $r = [κ : k]$ , and let $π ⁣ : S^{'} = {Bl}_{p} S \to S$ be the blowup of $S$ at $p$ with exceptional subscheme $E$ . (Point blowups of regular surfaces stay regular, with rational exceptional fibre over the residue field)

[F10]

lem-nonaffine-rational-map-normal-to-proper-codimension-two. Assume the Axiom of Choice. Let $X$ be a normal integral finite-type $k$ -scheme and $Y$ a proper finite-type $k$ -scheme. The maximal domain of a rational map $f : X ⇢ Y$ contains every codimension-one point of $X$ . Thus its closed complement has codimension at least two, if nonempty. (A rational map from a normal variety to a proper variety extends in codimension one)

[F11]

thm-nakayama-lemma. Assume the Axiom of Choice. Let $R$ be a commutative ring, let $I ⊴ R$ satisfy $I \subseteq J (R)$ , and let $M$ be a finitely generated left $R$ -module. If $I M = M$ , then $M = 0$ . (Assuming the Axiom of Choice, Nakayama's lemma)

Proof

1.1F3F4F5given

Put $A = O_{Y, y}$ and localize the proper birational map at $y$ ; the normalized-point domination helper applied to the normalization of the dominant graph of the rational lift over $X_{A}$ produces a finite roof of ordinary point blowups of the regular surface $X_{A}$ , all over its closed fibre, on which the lift is a morphism. Each centre lies over the closed point $y$ and has residue field finite over $κ (y)$ , so it is closed in the corresponding global model of $X$ . Point ideals localize, so the same finite sequence can be made globally on $X$ , retaining the lift over $A$ ; the exceptional curves and their conormal bundles are consequently those of point blowups of regular finite-type $k$ -surfaces.

2.1F6F9step 1.1

Choose a roof with the least number $n$ of point blowups. If $n > 0$ , let $E$ be the last exceptional curve and $g$ the induced morphism to the target blowup; if $g (E)$ were a point, the universal property of a contraction would descend $g$ through the last point blowup, contradicting minimality.

3.1F2F7F10step 2.1

Hence $g (E)$ is the target exceptional curve $E^{'}$ , and $E \to E^{'}$ is birational because $g$ is an isomorphism in codimension one; a proper nonconstant map of integral curves is quasi-finite and therefore finite, and a finite birational map over a normal affine chart equals that chart, so $E \to E^{'}$ is an isomorphism. Their conormal bundles are both $O (1)$ over the common constant field. The induced map is nonzero because $g$ is an isomorphism near the generic point of $E$ ; a nonzero map between these equal-degree line bundles is multiplication by a nonzero constant, hence is an isomorphism, and at every point local equations satisfy $g^{*} v^{'} = u v$ with $u$ a unit.

4.1F7F11step 3.1

Consequently the maximal ideal at each point of $E$ is generated by the image of the target maximal ideal together with the local equation of $E$ , and the residue field is finite, so $g$ is quasi-finite at every point of $E$ ; the quasi-finite-point helper makes $g$ an isomorphism over a neighbourhood of every point of $E^{'}$ , so the inverse image of $E^{'}$ is exactly $E$ . Its image in $X_{A}$ is the last centre, so the original fibre over $y$ is a singleton and $f$ is quasi-finite there, hence an isomorphism near $y$ by the same helper, contradicting that the inverse is undefined at $y$ .

5.1F1F8step 4.1∎

Therefore $n = 0$ and the rational lift is already a morphism on $X_{A}$ , so the centre ideal pulls back to an invertible ideal there; globally the noninvertible locus is closed and lies over $y$ , hence is empty, so the ideal is invertible on $X$ and the universal property of the blowup gives the required unique factorization $g ⁣ : X \to {Bl}_{y} Y$ . The Axiom of Choice is inherited from the cited suppliers.

Remarks

The roof and conormal argument works over every residue field; no rational point of the exceptional curve is chosen.
Uniqueness of g follows because two lifts agree on the common generic open, which is dense and reduced.

Depends on

Used by

Dependency tree · two levels

136 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.17 (Factorization birational maps) (standard reference, not scraped)
The Stacks Project, Resolution of Surfaces, Lemma 54.3.1 (Blowing up a regular surface at a point) (standard reference, not scraped)
The Stacks Project, Resolution of Surfaces, Lemma 54.4.3 (Rational maps dominated by quadratic transformations) (standard reference, not scraped)
Olivier Debarre, Introduction to Mori Theory (M2 course notes, 2016 version) (standard reference, not scraped)