LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-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.

Universal property of an affine blowup chart

Statement

Let $φ ⁣ : A \to B$ be a ring map, $I \subseteq A$ an ideal and $a \in I$ ; suppose the image $b = φ (a)$ is a nonzerodivisor in $B$ and $I B = b B$ . Then there is a unique $A$ -algebra homomorphism $A [I / a] \to B$ sending $x / a^{n}$ to the unique $y \in B$ with $x = b^{n} y$ ( $x \in I^{n}$ ); equivalently, $Spec B \to Spec A [I / a]$ is the unique $A$ -morphism into the chart $Spec A [I / a]$ along which the image of $a$ generates $I O_{Spec B}$ . The chart $A [I / a]$ itself satisfies the hypothesis with $b$ the image of $a$ .

Facts & Assumptions

Given: A commutative ring $A$ , an ideal $I \subseteq A$ , an element $a \in I$ , a ring map $φ ⁣ : A \to B$ whose image $b = φ (a)$ is a nonzerodivisor in $B$ and satisfies $I B = b B$ , and the affine blowup algebra $A [I / a]$ of (Affine blowup algebras: normal form, nonzerodivisors, reducedness, domains) built from the Rees algebra $R (I) = ⨁_{n \geq 0} I^{n} t^{n}$ of (The Rees algebra of an ideal and the Rees module of a filtered module).

[F1]

Affine blowup algebras: normal form, nonzerodivisors, reducedness, domains: For a commutative ring $A$ , an ideal $I \subseteq A$ and $a \in I$ , the affine blowup algebra $A [I / a] : = (R (I))_{(a)}$ is the degree-zero part of the localisation of the Rees algebra $R (I)$ at the multiplicative set generated by $a t$ ; the image of $a$ in $A [I / a]$ is a nonzerodivisor and $I A [I / a] = a A [I / a]$ .

[F2]

The Rees algebra of an ideal and the Rees module of a filtered module: For a commutative ring $R$ and an ideal $I \subset R$ , the Rees algebra is the graded subring $R (I) = ⨁_{n \geq 0} I^{n} t^{n} \subset R [t]$ ; equivalently, it is the graded ring whose degree- $n$ piece is $I^{n}$ .

[F3]

Multiplicative subsets and the localisation $S^{- 1} R$ as equivalence classes of fractions: For a commutative ring $R$ and a multiplicative subset $S \subseteq R$ , the localisation $S^{- 1} R$ has elements written $r / s$ with $r / s = r^{'} / s^{'}$ if and only if $u (r s^{'} - r^{'} s) = 0$ for some $u \in S$ ; the operations are $r / s + r^{'} / s^{'} = (r s^{'} + r^{'} s) / (s s^{'})$ and $(r / s) (r^{'} / s^{'}) = r r^{'} / (s s^{'})$ ; every $s \in S$ maps to a unit.

Proof

1.1F1F2F3given

Put $β = φ (a)$ . By the fraction description of the affine blowup algebra, every element of $C = A [I / a]$ has the form $r / a^{n}$ , $r \in I^{n}$ , and $r / a^{n} = s / a^{m}$ precisely when $a^{k} (a^{m} r - a^{n} s) = 0$ for some $k \geq 0$ . Since $I^{n} B = (I B)^{n} = β^{n} B$ , there is a unique $y \in B$ with $φ (r) = β^{n} y$ : existence follows from this ideal equality and uniqueness from the nonzerodivisor hypothesis on $β$ .

2.1step 1.1

Define $ψ (r / a^{n}) = y$ . If $r / a^{n} = s / a^{m}$ , write $φ (r) = β^{n} y$ and $φ (s) = β^{m} z$ . Applying $φ$ to the equality criterion gives $β^{k + m + n} (y - z) = 0$ , hence $y = z$ . Thus $ψ$ is well defined. The numerator of the sum is $a^{m} r + a^{n} s$ , whose image is $β^{m + n} (y + z)$ ; the product numerator $r s$ has image $β^{m + n} y z$ . Uniqueness of division by $β^{m + n}$ proves additivity and multiplicativity. Degree-zero fractions show that $ψ$ restricts to $φ$ on $A$ and sends $1$ to $1$ .

3.1F1step 2.1∎

Any $A$ -algebra map $χ : C \to B$ satisfies $β^{n} χ (r / a^{n}) = φ (r)$ , because $a^{n} (r / a^{n}) = r$ in $C$ . Cancellation of $β^{n}$ forces $χ (r / a^{n}) = ψ (r / a^{n})$ for every fraction. Hence the map is unique among all $A$ -algebra maps. The chart itself has $I C = a C$ with $a$ a nonzerodivisor, and the affine scheme/ring correspondence gives the stated geometric formulation.

Depends on

Used by

Universal property of the blowup Theorem

Dependency tree · two levels

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