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.

Two charts of the blowup of the affine plane at the origin

Example

Let $k$ be a field and consider ${Bl}_{0} A^{2}$ for the ideal $(x, y)$ . The two standard charts are $Spec k [x, y] [y / x] = Spec k [x, y / x]$ and $Spec k [x / y, y]$ , each isomorphic to $A_{k}^{2}$ , glued along the overlap $D (y / x) \leftrightarrow D (x / y)$ with $(y / x) (x / y) = 1$ ; the exceptional curve $E$ is cut by $x$ in the first chart and by $y$ in the second, and the projection to $A_{k}^{2}$ is the identity on the complement of $E$ and contracts $E$ to the origin. The total transform of a line through the origin is (the strict transform of the line) $+ E$ .

Facts & Assumptions

Given: A field $k$ , the scheme $A_{k}^{2} = Spec k [x, y]$ , the ideal $(x, y)$ and its blowup.

[A1]

Choice. The Axiom of Choice is assumed as inherited from the relative Proj construction; no further choice is used in this computation.

[F1]

The blowup of the plane at the origin as an incidence scheme: With homogeneous coordinates $u, v$ on $P_{k}^{1}$ , the blowup is $V (x v - y u) \subseteq A_{k}^{2} \times_{k} P_{k}^{1}$ with structural morphism as projection; its two standard charts are $Spec k [x, T]$ with $y = x T$ and $Spec k [y, U]$ with $x = y U$ , their overlap inverts $T$ and $U$ with $T U = 1$ , and the exceptional divisor is $V (x)$ and $V (y)$ respectively and is $P_{k}^{1}$ .

[F2]

Affine blowup standard charts and overlaps: For $I = (x, y)$ in $k [x, y]$ , the standard opens $Spec k [x, y] [I / x]$ and $Spec k [x, y] [I / y]$ cover the blowup, with transition map $u_{x y} = y / x \mapsto u_{y x}^{- 1}$ , where $u_{y x} = x / y$ on the overlap.

[F3]

Affine blowup algebras: normal form, nonzerodivisors, reducedness, domains: $A [I / a]$ has $I A [I / a] = a A [I / a]$ and $(A [I / a])_{a} = A_{a}$ .

[F5]

Relative projective space from standard charts: $P_{k}^{1}$ is covered by the two standard affine charts $Spec k [T]$ and $Spec k [U]$ with overlap $T U = 1$ .

Verification

1.1A1F1F2

The blowup is $V (x v - y u) \subseteq A_{k}^{2} \times_{k} P_{k}^{1}$ by [F1], and its two standard charts are $Spec k [x, T]$ with $y = x T$ and $Spec k [y, U]$ with $x = y U$ ; these are exactly the affine blowup algebras $k [x, y] [I / x]$ and $k [x, y] [I / y]$ of [F2] and [F3], and by [F5] the two charts of $P_{k}^{1}$ glue along $T U = 1$ .

2.1F2F3step 1.1

Each chart ring is a polynomial ring in two variables over $k$ , namely $k [x, T] ≅ k [x, y / x]$ and $k [y, U] ≅ k [x / y, y]$ , so $Spec k [x, y] [I / x] = Spec k [x, T] ≅ A_{k}^{2}$ and $Spec k [y, U] ≅ A_{k}^{2}$ ; the overlap is the open subscheme $D (T) = D (U^{- 1})$ of the first chart, identified with $D (U)$ in the second by $T \mapsto U^{- 1}$ .

3.1F1F5step 2.1

By [F1] the exceptional divisor is cut by $x$ in the first chart and by $y$ in the second, and it is $P_{k}^{1}$ : in the first chart $E \cap {x \neq 0}$ is empty and $E$ is the line $V (x) ≅ Spec k [T]$ , in the second $E = V (y) ≅ Spec k [U]$ , and the two affine lines glue along $T U = 1$ by [F5].

4.1step 2.1step 3.1

The projection sends the first chart to $A_{k}^{2}$ by $(x, T) \mapsto (x, x T)$ and the second by $(y, U) \mapsto (y U, y)$ : on the open locus $x \neq 0$ of the first chart the formula is inverted by $T = y / x$ , so the projection restricts to an isomorphism onto ${(x, y) : x \neq 0}$ , and symmetrically the second chart is isomorphic to ${(x, y) : y \neq 0}$ over the base. These two open subschemes cover $A_{k}^{2} ∖ {0}$ and the inverses agree on the overlap because $T = U^{- 1}$ there (step 2.1), so the projection is the identity over $A_{k}^{2} ∖ {0}$ . It contracts $E$ to the origin: on $E$ the first chart has $x = 0$ and image $(0, 0)$ , and on the second $y = 0$ and image $(0, 0)$ , while every point of $E$ lies in one of the two charts (step 3.1).

5.1F1F3step 1.1∎

Let $L = V (ℓ)$ be a line through the origin and first suppose $ℓ = y - a x$ with $a \in k$ . In the first chart the pulled-back equation is $x T - a x = x (T - a)$ , so the pullback divisor is the sum of $E = V (x)$ and the strict transform $V (T - a)$ ; in the second chart it is $y - a y U = y (1 - a U)$ , the sum of $E = V (y)$ and $V (1 - a U)$ , and for $a \neq 0$ the two strict-transform pieces glue at the same exceptional point with coordinates $T = a$ , $U = a^{- 1}$ ; for $a = 0$ the second piece is empty and the exceptional intersection is $T = 0$ . For the vertical line $ℓ = x$ the first chart gives $x$ , namely $E$ , and the second gives $y U$ , namely $E$ plus the strict transform $V (U)$ ; so in both cases the total transform is the strict transform plus $E$ , with multiplicity one along $E$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

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)
Roman Bezrukavnikov et al., MIT 18.725 Algebraic Geometry (Fall 2015) consolidated lecture notes (standard reference, not scraped)