Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Affine blowup standard charts and overlaps

Statement

Assume the Axiom of Choice as inherited from the Proj construction. Let A be a ring, I=(f0,…,fr)⊆A, S=R(I)=⨁Intn and Bi=A[I/fi]=(S[(fit)−1])0. The standard opens Ui=D+(fit)=Spec⁡Bi cover Bl⁡ISpec⁡A. Put uij=(fjt)/(fit) in Bi. Then Ui∩Uj=D(uij) in Ui, with canonical A-algebra identifications (Bi)uij=S[(fit)−1,(fjt)−1]0=(Bj)uji. They send fl/fi to (fl/fj)/(fi/fj), and uij to uji−1. These identifications satisfy the identity and cocycle conditions and preserve the structural maps to Spec⁡A. Different finite generating families give compatible chart covers of the same canonical blowup; no bijection between the chart families is asserted. The formulas include zero divisors and empty charts; nilpotent fi gives Bi=0. Localization at the base element fj is generally smaller than this overlap and is not its formula.

Facts & Assumptions

Given: A ring A, an ideal I=(f0,…,fr)⊆A, the Rees algebra S=R(I)=⨁n≥0Intn (Rees algebra sheaf of a finite type ideal), the blowup Bl⁡ISpec⁡A (Blowup of a scheme along an ideal sheaf), and the Axiom of Choice as inherited from the Proj construction (The Axiom of Choice).

[F1]

Blowup of a scheme along an ideal sheaf: For X=Spec⁡A and I=I~, the blowup is the absolute Proj of the Rees algebra R(I)=⨁n≥0Intn, with structural morphism to Spec⁡A.

[F2]

Affine blowup algebras: normal form, nonzerodivisors, reducedness, domains: For a ring A, an ideal I⊆A and a∈I, the affine blowup algebra is A[I/a]=(R(I))(a), the degree-zero part of the localisation of R(I) at the multiplicative set generated by at.

[F3]

Proj carries a scheme structure: For a commutative nonnegatively graded ring S, Proj⁡S carries open subscheme identifications φf ⁣:D+(f)→Spec⁡S(f) for homogeneous f∈S+, the D+(f) form an affine open cover, and for homogeneous f,g of degrees d,e the set D+(f)∩D+(g)=D+(fg) is carried by φf onto D(gd/fe)⊆Spec⁡S(f), with transition induced by S(f)[(gd/fe)−1]≅S(fg)≅S(g)[(fe/gd)−1]; the underlying space is Proj⁡S with the standard-open basis, the scheme is unique for these identifications, and if f is nilpotent then D+(f)=∅ and S(f)=0.

[F4]

Standard opens of Proj: For homogeneous f∈S+, D+(f)={p∈Proj⁡S:f∉p} is a standard open.

[F5]

Standard opens are affine: The canonical chart map φf ⁣:D+(f)→Spec⁡S(f) is an isomorphism, including the empty case: nilpotent f gives D+(f)=∅ and S(f)=0.

Proof

1.1F1F2F3F4F5

Put gi=fit∈S, a homogeneous element of degree one, so that S=R(I)=A[It] is generated as an A-algebra by I, and S+ is generated as an ideal by g0,…,gr; hence no homogeneous prime p of S contains all gi without containing S+, and the standard opens D+(gi) cover Proj⁡S=Bl⁡ISpec⁡A by [F1], [F3], [F4]. Moreover Bi=A[I/fi]=S(gi) by [F2], so Ui=D+(gi)=Spec⁡Bi by [F5].

2.1F3F5step 1.1

For each pair i,j, [F3] applied to the degree-one elements gi,gj identifies D+(gi)∩D+(gj)=D+(gigj) with D(uij)⊆Spec⁡Bi, where uij=gj/gi, and identifies the two charts through the canonical isomorphisms Bi[uij−1]=S(gi)[(gj/gi)−1]≅S(gigj)≅S(gj)[(gi/gj)−1]=(Bj)uji.

3.1F3step 2.1

The identification of step 2.1 can be checked directly and torsion-safely: the canonical map Bi[uij−1]→(S[gi−1,gj−1])0 is surjective, because a degree-zero fraction c/(gimgjn) with c homogeneous of degree m+n equals (c/gim+n)uij−n with c/gim+n∈Bi; and it is injective, because vanishing of the image means gipgjqc=0 in S for some p,q≥0, whence uijq(c/gim)=gipcgjq/gim+p+q=0 in Bi[uij−1]. No cancellation of gi in S is used. The same identification sends fl/fi=(flt)/(fit) to (flt)/(fit) computed in S(gigj), which equals (fl/fj)/(fi/fj), and sends uij=gj/gi to uji−1.

4.1F3step 2.1step 3.1

The identifications satisfy the identity condition (for i=j, uii=1 and the transition is the identity) and the cocycle condition: on a triple overlap every transition is induced by the localisation map S→S[gi−1,gj−1,gk−1] and taking degree zero, so the three compositions around the cycle coincide with the identity on S(gigjgk). They preserve the structural maps to Spec⁡A, because they are isomorphisms of A-algebras for the structure maps A=S0→S(g) of the charts.

4.2F2step 2.1step 3.1

For I=(x,y)⊆A=k[x,y] with f0=x, f1=y, one has B0=A[I/x]=k[x,y/x]=k[x,s] with s=y/x and y=xs, and u01=s, so the overlap D(u01)=D(s) in Spec⁡B0 retains the points with x=0 and s≠0. Localising instead at the base element f1=y gives D(y)=D(xs)=D(x)∩D(s), which is strictly smaller than D(s) and omits those points; hence localisation at the base element is not the overlap formula.

5.1F3step 4.1

A second finite generating family I=(h0,…,hr′) gives the charts D+(hkt)=Spec⁡A[I/hk] of the same scheme Proj⁡S, with their own overlap identifications supplied by the same formulas of [F3] applied to the degree-one elements of S; on the intersection of a chart of the first family and a chart of the second, D+(gi)∩D+(hkt)=D+(gihkt), the transition is again induced by the canonical localisation of S, so the two cover structures are compatible. No bijection between the two chart families is asserted: the charts are indexed by different generating sets and need not correspond individually.

6.1F3F5step 5.1∎

The formulas allow zero divisors and empty charts: step 3.1 never cancels gi in S, and if fi is nilpotent then gi=fit is nilpotent, so D+(gi)=∅ and Bi=S(gi)=0 by [F3] and [F5]; the same holds for the overlap formula in the degenerate cases. This completes the proof.

Depends on

Used by

Dependency tree · two levels

25 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