The blowup of an affine scheme away from its center

Let I be an ideal of a commutative ring R. The blowup of Spec R along V(I) is Proj R[It] ⟶ Spec R. This file proves that it changes nothing away from the center: over every open subset of Spec R disjoint from V(I) it restricts to an isomorphism.

Locally this is explicit. For a ∈ I, the part of the blowup lying over the basic open D(a) is the basic open D(a) of the chart Spec R[I/a], and over it the chart is Spec of the isomorphism R_a ≅ R[I/a]_a: the compatible tower R → R[I/a] ↪ R_a identifies the localization of the intermediate algebra at a with R_a; the map from R need not be injective.

For instance, if π ∈ I, this applies to U = D(π): blowing up a center contained in V(π) changes nothing over D(π). When R is an algebra over a discrete valuation ring with uniformizer π, the open D(π) is the generic fibre. The isomorphism over this open preserves the generic-fibre identification; no flatness assertion is made here.

When I is finitely generated, the blowup is moreover proper over Spec R.

Main results

All results are in the namespace TauCeti.AlgebraicGeometry.

• toSpecZero_reesAlgebra_preimage_basicOpen: the inverse image of D(a) in the blowup is the standard open D₊(a) of the degree-zero element a.
• affineBlowupι_image_basicOpen: for a ∈ I, the inverse image of D(a) in the blowup is the image of the basic open D(a) of the chart Spec R[I/a].
• isIso_morphismRestrict_toSpecZero_reesAlgebra_of_disjoint_zeroLocus: the blowup Proj R[It] ⟶ Spec R restricts to an isomorphism over every open subset of Spec R that is disjoint from V(I).
• isProper_toSpecZero_reesAlgebra: for finitely generated I, the blowup Proj R[It] ⟶ Spec R is proper.

References

• The Stacks Project, Section Blowing up

theorem TauCeti.AlgebraicGeometry.toSpecZero_reesAlgebra_preimage_basicOpen {R : Type u} [CommRing R] (I : Ideal R) (a : R) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)).base).obj (PrimeSpectrum.basicOpen a) = AlgebraicGeometry.Proj.basicOpen (reesAlgebra.grade I) ↑((reesAlgebra.gradeZeroEquiv I) a)

The inverse image of the basic open D(a) of Spec R in the blowup Proj R[It] is the standard open D₊(a) of the degree-zero element a: the homogeneous primes not containing a.

theorem TauCeti.AlgebraicGeometry.affineBlowupι_image_basicOpen {R : Type u} [CommRing R] {I : Ideal R} {a : R} (S : Type u) [CommRing S] [Algebra R S] [IsLocalization.Away a S] (ha : a ∈ I) : (AlgebraicGeometry.Scheme.Hom.opensFunctor (affineBlowupι S ha)).obj (PrimeSpectrum.basicOpen ((algebraMap R ↥(I.affineBlowup a S)) a)) = (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)).base).obj (PrimeSpectrum.basicOpen a)

The blowup over D(a). For a ∈ I, the inverse image of the basic open D(a) of Spec R in the blowup Proj R[It] is the image of the basic open D(a) of the chart Spec R[I/a].

theorem TauCeti.AlgebraicGeometry.isIso_morphismRestrict_toSpecZero_reesAlgebra_of_disjoint_zeroLocus {R : Type u} [CommRing R] {I : Ideal R} {U : (AlgebraicGeometry.Spec ↧R).Opens} (hU : Disjoint (↑U) (PrimeSpectrum.zeroLocus ↑I)) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom) ∣_ U)

The blowup is an isomorphism away from its center. The blowup Proj R[It] ⟶ Spec R of Spec R along V(I) restricts to an isomorphism over every open subset U of Spec R that is disjoint from V(I).

theorem TauCeti.AlgebraicGeometry.isProper_toSpecZero_reesAlgebra {R : Type u} [CommRing R] {I : Ideal R} (hI : I.FG) : AlgebraicGeometry.IsProper (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom))

The blowup along a finitely generated ideal is proper. If I is finitely generated, the blowup Proj R[It] ⟶ Spec R of Spec R along V(I) is proper.