ExampleConstruction: AI-generatedVerification: 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.

Blowing up the empty center is the identity

Example

Let $X$ be a scheme and let $I = O_{X}$ be the unit ideal sheaf, whose zero scheme $V (O_{X})$ is empty. Then the blowup is ${Bl}_{O_{X}} X = {Proj}_{X} R (O_{X}) = {Proj}_{X} O_{X} [t] = X$ : the relative Proj of the polynomial algebra in one degree-one variable is the base, and the structural morphism is the identity. Equivalently, the unit ideal is invertible and defines the empty effective Cartier divisor, so blowing up the empty center changes nothing.

Facts & Assumptions

Given: A scheme $X$ , the unit ideal sheaf $I = O_{X}$ , and the blowup $π ⁣ : {Bl}_{O_{X}} X \to X$ of Blowup of a scheme along an ideal sheaf.

[A1]

Choice. The Axiom of Choice is inherited from the relative Proj construction used to form the blowup; no further choice is used below.

[F1]

Blowup of a scheme along an ideal sheaf: Let $X$ be a scheme and let $I \subseteq O_{X}$ be a quasi-coherent ideal sheaf of finite type, with zero scheme $Z = V (I)$ , the closed subscheme of $X$ cut out by $I$ . The blowup of $X$ along $I$ is the $X$ -scheme ${Bl}_{I} X : = {Proj}_{X} R (I)$ , the relative Proj of the Rees algebra sheaf $R (I) = ⨁_{n \geq 0} I^{n}$ , with its structural morphism $π$ to $X$ .

[F2]

Rees algebra sheaf of a finite type ideal: The Rees algebra sheaf $R (I) = ⨁_{n \geq 0} I^{n}$ is a commutative graded $O_{X}$ -algebra with $R (I)_{0} = O_{X}$ and $R (I)_{1} = I$ . If $U = Spec A \subseteq X$ is affine and $I ∣_{U} = \tilde{I}$ for an ideal $I \subseteq A$ , then $I^{n} ∣_{U} = \tilde{I^{n}}$ for every $n \geq 0$ , and taking sections on $U$ gives the affine Rees algebra $⨁_{n \geq 0} I^{n} t^{n}$ .

[F3]

Affine blowup standard charts and overlaps: Let $A$ be a ring, $I = (f_{0}, \dots, f_{r}) \subseteq A$ , $S = R (I) = ⨁ I^{n} t^{n}$ and $B_{i} = A [I / f_{i}] = (S [(f_{i} t)^{- 1}])_{0}$ . The standard opens $U_{i} = D_{+} (f_{i} t) = Spec B_{i}$ cover ${Bl}_{I} Spec A$ .

[F4]

Blowing up an effective Cartier divisor does nothing: The blowup of a scheme along an invertible ideal sheaf, equivalently along an effective Cartier divisor, is the identity: its structural morphism is an isomorphism.

[F5]

Effective cartier divisor: A unit equation, in particular $f_{i} = 1$ , gives the zero Cartier divisor with ideal sheaf $O_{X}$ ; it is the empty effective divisor, and its vanishing subscheme is empty.

Verification

1.1F2

Since $I = O_{X}$ is the unit ideal, $I^{n} = I \cdot \dots \cdot I = O_{X}$ for every $n \geq 0$ , so $R (O_{X}) = ⨁_{n \geq 0} O_{X}$ . On an affine open $U = Spec A \subseteq X$ the ideal is $I ∣_{U} = \tilde{A}$ , and the affine Rees algebra is $⨁_{n \geq 0} A \cdot t^{n} = A [t]$ with $t$ of degree one, by [F2]; these identifications are compatible with restriction to smaller affine opens, so they glue to a canonical isomorphism $R (O_{X}) ≅ O_{X} [t]$ of graded $O_{X}$ -algebras, where $t$ is a degree-one generator.

2.1F1step 1.1

By the definition of the blowup, ${Bl}_{O_{X}} X = {Proj}_{X} R (O_{X}) = {Proj}_{X} O_{X} [t]$ , the relative Proj of the graded $O_{X}$ -algebra computed in step 1.1, with the structural morphism to $X$ .

2.2F3step 1.1

The structural morphism ${Proj}_{X} O_{X} [t] \to X$ is an isomorphism. Indeed, let $U = Spec A \subseteq X$ be an affine open and restrict to $U$ , where the graded algebra is $A [t]$ with the unit ideal generated by the single element $f_{0} = 1$ ; the generating family $(1)$ has one element, and [F3] gives the single standard chart $D_{+} (t) = Spec B_{0}$ with $B_{0} = A [I / 1] = (A [t] [t^{- 1}])_{0} = A$ , since a degree-zero element of $A [t, t^{- 1}]$ is its constant term. Its structure map to $Spec A$ is the identity, the chart covers the blowup over $U$ , and the identifications for different affine opens are the canonical restrictions of the same $t$ , so they agree on overlaps and glue to an inverse of the structural morphism.

3.1F4F5step 2.1step 2.2∎

Equivalently, $O_{X}$ is invertible and the unit equation $1$ exhibits the center $V (O_{X})$ as the empty effective Cartier divisor with ideal sheaf $O_{X}$ on every affine chart, so [F4] gives directly that the blowup is the identity. Combining with steps 2.1 and 2.2, ${Bl}_{O_{X}} X = {Proj}_{X} R (O_{X}) = {Proj}_{X} O_{X} [t] = X$ and the structural morphism is the identity; the zero scheme $V (O_{X})$ is empty, so blowing up the empty center changes nothing.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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, Commutative Algebra, Section 10.70 (Blow up algebras) (standard reference, not scraped)
The Stacks Project, Divisors, Sections 31.33-31.36 (Blowing up; Strict transform; Admissible blowups; Blowing up and flatness) (standard reference, not scraped)