The affine charts of the blowup of an affine scheme

The blowup of Spec R along the closed subscheme V(I) cut out by an ideal I is Proj R[It], the Proj of the Rees algebra with its grading reesAlgebra.grade I. This file describes it by explicit affine charts: for a ∈ I there is an open immersion

Spec R[I/a] ⟶ Proj R[It]

from the spectrum of the affine blowup algebra R[I/a] ⊆ R_a onto the standard open D₊(a t), compatible with the structure maps to Spec R; and if I is generated by a family s, the charts of the sᵢ cover Proj R[It]. This is the description of the blowup by the algebras R[I/a] of TauCeti/RingTheory/Ideal/AffineBlowup.lean, through which local computations with blowups, such as the blowup of the node xy = πⁿ at its singular point, are carried out.

Main definitions

• TauCeti.AlgebraicGeometry.affineBlowupι S ha: the open immersion Spec R[I/a] ⟶ Proj R[It], for a ∈ I and a localization S of R away from a.

Main results

• TauCeti.AlgebraicGeometry.opensRange_affineBlowupι: the chart of a is an open immersion onto the standard open D₊(a t).
• TauCeti.AlgebraicGeometry.iSup_opensRange_affineBlowupι: if I is generated by a family s, the charts of the sᵢ cover Proj R[It].
• TauCeti.AlgebraicGeometry.affineBlowupι_toSpecZero: the chart is a morphism over Spec R.

References

• The Stacks Project, Section Blowing up, in particular Lemma 0804 for the affine charts.

noncomputable def TauCeti.AlgebraicGeometry.affineBlowupι {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.Spec ↧↥(I.affineBlowup a S) ⟶ AlgebraicGeometry.Proj (reesAlgebra.grade I)

The affine chart of the blowup. For a ∈ I, the open immersion Spec R[I/a] ⟶ Proj R[It] from the spectrum of the affine blowup algebra R[I/a] onto the standard open D₊(a t) of the blowup Proj R[It] of Spec R along V(I).

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.AlgebraicGeometry.instIsOpenImmersionAffineBlowupι {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.IsOpenImmersion (affineBlowupι S ha)

theorem TauCeti.AlgebraicGeometry.opensRange_affineBlowupι {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.opensRange (affineBlowupι S ha) = AlgebraicGeometry.Proj.basicOpen (reesAlgebra.grade I) (reesAlgebra.monomialDegreeOne ha)

The chart Spec R[I/a] ⟶ Proj R[It] is an open immersion onto D₊(a t).

theorem TauCeti.AlgebraicGeometry.iSup_opensRange_affineBlowupι {R : Type u} [CommRing R] {I : Ideal R} {ι : Type u_1} {s : ι → R} (hs : Ideal.span (Set.range s) = I) : ⨆ (i : ι), AlgebraicGeometry.Scheme.Hom.opensRange (affineBlowupι (Localization.Away (s i)) ⋯) = ⊤

The affine charts cover the blowup. If the ideal I is generated by a family s, then the charts Spec R[I/sᵢ] ⟶ Proj R[It] cover the blowup Proj R[It].

theorem TauCeti.AlgebraicGeometry.affineBlowupι_toSpecZero {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) : CategoryTheory.CategoryStruct.comp (affineBlowupι S ha) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↥(I.affineBlowup a S)))

The chart Spec R[I/a] ⟶ Proj R[It] is a morphism over Spec R: followed by the structure map of the blowup, it is the spectrum of the structure map R → R[I/a]. Here Spec R is identified with the spectrum of the degree zero part of R[It].

theorem TauCeti.AlgebraicGeometry.affineBlowupι_toSpecZero_assoc {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) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineBlowupι S ha) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom) h)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↥(I.affineBlowup a S)))) h

The chart Spec R[I/a] ⟶ Proj R[It] is a morphism over Spec R: followed by the structure map of the blowup, it is the spectrum of the structure map R → R[I/a]. Here Spec R is identified with the spectrum of the degree zero part of R[It].