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 I and I^2 give the same scheme

Example

Let $A$ be a ring and $I = (x, y) \subseteq A [x, y]$ the ideal of the origin. Then ${Bl}_{I} A^{2}$ and ${Bl}_{I^{2}} A^{2}$ are canonically isomorphic: the Rees algebra $R (I^{2})$ is the Veronese subalgebra of $R (I)$ in even degrees, and $Proj$ is invariant under Veronese regrading. Concretely ${Bl}_{I} A^{2}$ is the closed subscheme $V (x T_{1} - y T_{0})$ of $A^{2} \times P^{1}$ , and the second description uses the degree-two generators $x^{2}, x y, y^{2}$ with the relations they satisfy (the degree-two Veronese re-embedding of the same blowup).

Facts & Assumptions

Given: A ring $A$ , the polynomial ring $A [x, y]$ , the ideal $I = (x, y)$ of the origin, and its blowups.

[A1]

Choice. The Axiom of Choice is assumed as inherited from the Proj and Rees-algebra constructions; the identifications below inherit it.

[F1]

Blowing up I and I^d agree: Assume the Axiom of Choice. For a quasi-coherent ideal sheaf $I$ of finite type on $X$ and $d \geq 1$ there is a canonical isomorphism of $X$ -schemes ${Bl}_{I^{d}} X \to {Bl}_{I} X$ ; more precisely $R (I^{d})$ is the Veronese subalgebra $R (I)^{(d)}$ , and the canonical identification $Proj R (I) = Proj R (I)^{(d)}$ glues over $X$ .

[F2]

Rees algebra sheaf of a finite type ideal: $R (I) = ⨁_{n \geq 0} I^{n}$ with $I^{0} = O_{X}$ and multiplication induced by multiplication of ideals; its degree- $n$ piece is $I^{n}$ .

[F3]

Proj is invariant under Veronese regrading: For a commutative nonnegatively graded ring $S$ and $d \geq 1$ , there is a canonical isomorphism $Proj S ≅ Proj S^{(d)}$ mapping the chart $D_{+} (f)$ to $D_{+} (f^{d})$ with the same coordinate ring $S_{(f)} = S_{(f^{d})}^{(d)}$ , and carrying $O_{Proj S^{(d)}} (1)$ to $O_{Proj S} (d)$ ; for $d = 1$ it is the identity.

[F4]

Affine blowup standard charts and overlaps: For $I = (f_{0}, \dots, f_{r}) \subseteq A$ the charts $Spec A [I / f_{i}]$ cover ${Bl}_{I} Spec A$ with the displayed transition functions.

Verification

1.1F1F2F3

In the special case $d = 2$ of [F1], the Rees algebra of $I^{2}$ has degree- $n$ piece $I^{2 n}$ , which by [F2] is exactly the degree- $2 n$ piece of $R (I)$ ; hence $R (I^{2}) = R (I)^{(2)}$ as graded algebras, and the canonical identification of Proj's from [F3] (with its identity on coordinate rings $S_{(f)} = S_{(f^{2})}^{(2)}$ ) glues by [F1] to a canonical isomorphism ${Bl}_{I^{2}} A^{2} \to {Bl}_{I} A^{2}$ over $A^{2}$ .

2.1F4step 1.1

Concretely, [F4] presents ${Bl}_{I} A^{2}$ by the two charts $A [x, y] [I / x] = A [x, y / x]$ and $A [x, y] [I / y] = A [x / y, y]$ , glued by inverting the ratio; in the first chart put $T = y / x$ , so the chart is $A [x, T]$ and its exceptional divisor is $V (x)$ . The chart of the same kind for $I^{2}$ is $A [x, y] [I^{2} / x^{2}]$ , and the degree-two generators $x^{2}, x y, y^{2}$ give the fractions $x y / x^{2} = y / x = T$ and $y^{2} / x^{2} = T^{2}$ , so this chart ring is $A [x, T]$ again; symmetrically the second charts agree as subrings of $A [x, x^{- 1}, y]$ and $A [y, y^{- 1}, x]$ . Writing $X, Y, Z$ for their degree-one Rees symbols, their relations include $X Z = Y^{2}$ , $x Y = y X$ and $x Z = y Y$ ; the Veronese identification in step 1.1 gives the same blowup. The two charts cover also the regraded Proj, since $X Z = Y^{2}$ prevents a homogeneous prime outside the irrelevant locus from containing both $X$ and $Z$ . Its original incidence description is checked directly: intersecting $V (x T_{1} - y T_{0}) \subseteq A^{2} \times P^{1}$ with the chart $T_{0} = 1$ gives $x T = y$ with $T = T_{1} / T_{0}$ , namely the first chart, and with $T_{1} = 1$ gives $x = y U$ , $U = T_{0} / T_{1}$ , namely the second, the two glued by $T U = 1$ .

3.1F1F3step 2.1∎

Thus the identity morphism on the underlying charts, read through the Veronese regrading of step 1.1, is the canonical isomorphism ${Bl}_{I} A^{2} ≅ {Bl}_{I^{2}} A^{2}$ , and the second description uses the degree-two generators $x^{2}, x y, y^{2}$ with their relation $X Z = Y^{2}$ (the degree-two Veronese conic in $P^{2}$ ) as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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)