Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
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.

The blowup is an isomorphism off the center

Statement

Let I be a quasi-coherent ideal sheaf of finite type with zero scheme Z and let π ⁣:Bl⁡IX→X be the blowup. Then the restriction π ⁣:π−1(X∖Z)→X∖Z is an isomorphism of schemes, with inverse characterized by the universal property applied to the identity of X∖Z (where the inverse image of Z is empty) and to the open immersion π−1(X∖Z)↪X. Consequently E=π−1(Z) is the complement of this open subscheme.

Facts & Assumptions

Given: A quasi-coherent ideal sheaf I of finite type with zero scheme Z, and the blowup π ⁣:Bl⁡IX→X.

[A1]

Choice. The Axiom of Choice is assumed as inherited from the blowup and Proj constructions used by the cited items.

[F1]

Affine blowup standard charts and overlaps: For I=(f0,…,fr)⊆A, the standard opens Spec⁡A[I/fi] cover Bl⁡ISpec⁡A, with transition functions uij↦uji−1.

[F2]

Affine blowup algebras: normal form, nonzerodivisors, reducedness, domains: For a∈I the affine blowup algebra satisfies I A[I/a]=a A[I/a] and (A[I/a])a=Aa, the latter being the ordinary localization of A at a.

[F3]

Blowup of a scheme along an ideal sheaf: Bl⁡IX=Proj⁡XR(I) with its structural morphism to X; the affine chart cover is supplied by [F1].

[F4]

Universal property of the blowup: For every X-scheme f ⁣:Y→X whose inverse image of Z is an effective Cartier divisor there is a unique X-morphism Y→Bl⁡IX.

[F5]

Effective cartier divisor: A unit equation represents the zero Cartier divisor, the empty effective divisor, and the empty scheme has only this effective divisor.

[F6]

Exceptional subscheme of a blowup: E=π−1(Z)=Z×XBl⁡IX with ideal sheaf IOBl⁡, and E is set-theoretically the preimage of Z.

Proof

1.1F1F2F3

Cover X by affine opens U=Spec⁡A with I∣U=(f0,…,fr); by [F1] and [F3] the preimage π−1(U) is covered by the charts Spec⁡A[I/fi], and by [F2] the chart ring localizes to Afi after inverting fi, and this chart contains the entire inverse image of D(fi). Indeed, in every chart j one has fi=fj(fi/fj); wherever fi is invertible, both fj and the ratio fi/fj are invertible. The ratio-overlap formula of [F1] puts this open of chart j in chart i. Thus the restriction of π over the principal open D(fi) is an isomorphism D(fi)→D(fi): it is the structural map Spec⁡A[I/fi]→Spec⁡A followed by localization, and (A[I/fi])fi=Afi.

2.1step 1.1

These local inverses glue. Let O and O′ be any two base opens of the form D(fi) in step 1.1, possibly in different affine base neighborhoods. The structural map on the whole inverse image π−1(O) is an isomorphism onto O. Restricting it to O∩O′ gives an isomorphism π−1(O∩O′)→O∩O′. Both local inverse maps restricted to this intersection land in that inverse image and are inverses of this same isomorphism, so they agree. Thus they glue to σ:X∖Z→W:=π−1(X∖Z) with π∘σ=id⁡. For two charts in one affine base, only the restriction of their chart overlap over D(fifj) is identified with D(fifj); the whole ratio overlap can also contain points over Z.

3.1step 2.1algebra

The morphism σ is an inverse for π∣W. Since X∖Z is covered by the opens D(fi) of step 1.1, and over each such open the restriction of σ is the inverse of the restriction of π (step 1.1), the composite σ∘π∣W agrees with id⁡W after restriction to the cover of W by the opens π−1(D(fi))∩Spec⁡A[I/fi], on each of which π is an isomorphism; hence σ∘π∣W=id⁡W and π∣W∘σ=id⁡X∖Z, so π∣W is an isomorphism.

4.1F4F5step 3.1

The inverse is characterized by the universal property: the inverse image of Z under the identity X∖Z→X is empty, hence the zero Cartier divisor, which is effective by [F5]; so [F4] gives a unique X-morphism τ ⁣:X∖Z→Bl⁡IX lifting the identity, and τ is an inverse of π over X∖Z; by uniqueness of the inverse of the isomorphism π∣W of step 3.1, τ=σ. In particular σ is the unique morphism over X from X∖Z into the blowup.

5.1F6step 3.1∎

Finally E is the complement of W: by [F6], E=π−1(Z) is set-theoretically the preimage of Z, so its underlying set is the complement of the underlying set of π−1(X∖Z)=W, i.e. E is the complement of the open subscheme W in the blowup.

Depends on

Used by

Dependency tree · two levels

30 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