ExampleConstruction: Literature-sourcedVerification: 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 a principal ideal of a nonzerodivisor does nothing

Example

Let $A$ be a ring and let $f \in A$ be a nonzerodivisor. Then the blowup of $Spec A$ along the principal ideal $(f)$ is $Spec A$ itself: the ideal sheaf $\tilde{(f)}$ is invertible and defines an effective Cartier divisor, and the single standard chart of the blowup has coordinate ring $A [(f) / f] = (R ((f)))_{(f t)} = A$ . All charts agree, because a principal ideal has a one-element generating family. Geometrically, blowing up an effective Cartier divisor, for example a $k$ -rational point of a regular curve or a line in the plane, gives back the same scheme.

Facts & Assumptions

Given: A ring $A$ , a nonzerodivisor $f \in A$ , the principal ideal $I = (f) \subseteq A$ , the closed subscheme $D = V (I) \subseteq Spec A$ , and the blowup $π ⁣ : {Bl}_{I} Spec A \to Spec A$ 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]

Effective cartier divisor: A Cartier divisor $D$ on a scheme $X$ is effective if it has a local-equation representation $(U_{i}, f_{i})$ with $f_{i} \in O_{X} (U_{i})$ and with multiplication by the germ $(f_{i})_{x}$ injective on $O_{X, x}$ for every $x \in U_{i}$ ; the local principal ideal sheaves $f_{i} O_{U_{i}}$ agree on overlaps and define the ideal sheaf $I_{D}$ of $D$ . A unit equation gives the zero Cartier divisor, the empty effective divisor, with ideal sheaf $O_{X}$ and empty vanishing subscheme.

[F2]

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}$ , equipped with its structural morphism $π$ to $X$ .

[F3]

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.

[F4]

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$ .

Verification

1.1F1given

In the notation of the given data, multiplication by $f$ defines an $A$ -module map $A \to I$ that is surjective because $I = (f)$ , and injective because $f$ is a nonzerodivisor; it is therefore an isomorphism, so $I$ is a free $A$ -module of rank one and the ideal sheaf $\tilde{I}$ is invertible. The same nonzerodivisor condition says that $f$ , read as the global local equation of $D = V (I)$ on $Spec A$ , is a regular section, so $D$ is an effective Cartier divisor with ideal sheaf $I_{D} = \tilde{I}$ .

2.1F3step 1.1

By step 1.1 the ideal sheaf $\tilde{I}$ is invertible, equivalently $D$ is an effective Cartier divisor with that ideal sheaf, so [F3] applies to the blowup of $Spec A$ along $I$ and shows that $π ⁣ : {Bl}_{I} Spec A \to Spec A$ is an isomorphism.

3.1F2F4

Independently of step 2.1, compute the chart: since $I = (f)$ , the Rees algebra is $R (I) = ⨁_{n \geq 0} (f)^{n} t^{n} = A [f t]$ , and the generating family $(f)$ has the single element $f$ , so the standard chart $D_{+} (f t)$ of the blowup is $Spec B_{0}$ with $B_{0} = A [I / f] = (A [f t] [(f t)^{- 1}])_{0}$ . An element of $A [f t] [(f t)^{- 1}] = A [f t, (f t)^{- 1}]$ is a finite sum $\sum_{k \in Z} a_{k} (f t)^{k}$ with $a_{k} \in A$ ; it has degree zero exactly when $a_{k} = 0$ for every $k \neq 0$ , so $B_{0} = A$ and $A [(f) / f] = A$ . The chart $D_{+} (f t)$ covers the whole blowup, so there are no other charts to compare.

4.1F1step 2.1step 3.1∎

Steps 2.1 and 3.1 agree: the blowup is $Spec A$ with identity structural morphism, and its single affine blowup algebra is $A [(f) / f] = A$ . The geometric instances named in the statement are covered by the same computation: the ideal of a $k$ -rational point of a regular curve is generated at that point by a uniformizer, hence by a nonzerodivisor equation of an effective Cartier divisor, and the ideal of a line in the plane is generated by a linear form, again a nonzerodivisor; blowing up either changes nothing.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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, Divisors, Sections 31.33-31.36 (Blowing up; Strict transform; Admissible blowups; Blowing up and flatness) (standard reference, not scraped)
Ravi Vakil, Foundations of Algebraic Geometry, June 27, 2011 draft (author-hosted 'Early (out-of-date) version of The Rising Sea') (standard reference, not scraped)