The charts of the affine blow-up

The affine blow-up Proj Rees(I) of Spec R along I is covered by the affine charts Spec R[I/a], a ∈ I, where R[I/a] ⊆ R_a is the subring of fractions x/aⁿ with x ∈ Iⁿ; for generators g₁, …, g_k of I the charts of the gᵢ suffice, and over the base the chart of a is Spec of the inclusion R → R[I/a] [Hau14, Theorem 4.19]; [TSPA, Tag 0804].

• affineBlowUp.chart I a : Spec R[I/a] ⟶ affineBlowUp I: Mathlib's open immersion Proj.awayι of the chart D₊(a t) composed with Spec of the chart ring isomorphism (Rees(I)_{at})₀ ≅ R[I/a] of Hironaka.Scheme.BlowUp.Rees.ChartRing. It is an open immersion with image the basic open D₊(a t) of Proj.
• affineBlowUp.affineOpenCover I: the charts for a ∈ I cover, from Mathlib's Proj.affineOpenCoverOfIrrelevantLESpan and the fact that the irrelevant ideal is generated in degree one (reesAlgebra.irrelevant_le_span_degreeOne); affineBlowUp.affineOpenCoverOfSpan s hs: the charts of any generating set s of I cover (Hauser's g₁, …, g_k), with the empty family for I = 0, whence affineBlowUp ⊥ is empty.
• affineBlowUp.chart_π: over the base the chart is Spec (R → R[I/a]), by Proj.awayι_toSpecZero and the constant-map compatibility of the chart ring isomorphism.
• affineBlowUp.chart_preimage_chart: inside the chart of a, the chart of b is the basic open D(b/a) ⊆ Spec R[I/a] — the identity D₊(at) ∩ D₊(bt) = D₊(at · bt) of Proj (Mathlib's Proj.awayι_preimage_basicOpen) transported along the chart ring isomorphism, under which Mathlib's localization element bt/at is b/a. This is the gluing of the charts along R_{g_j}, R_{g_l} ⊆ R_{g_j g_l} of [Hau14, Definition 4.13].

The underlying scheme is Mathlib's Proj; every statement here is a statement about Proj and its awayι charts read through the ring isomorphism of Hironaka.Scheme.BlowUp.Rees.ChartRing.

noncomputable def reesAlgebra.chartIso {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : ↧(HomogeneousLocalization.Away (grading I) ((degreeOne I) a)) ≅ ↧↥(AlgebraicGeometry.affineBlowUpAlgebra I ↑a)

The chart ring isomorphism (Rees(I)_{at})₀ ≅ R[I/a] (reesAlgebra.chartRingEquiv) as an isomorphism of CommRingCat.

Equations

• reesAlgebra.chartIso I a = (reesAlgebra.chartRingEquiv a).toCommRingCatIso

noncomputable def AlgebraicGeometry.affineBlowUp.chart {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : Spec ↧↥(affineBlowUpAlgebra I ↑a) ⟶ affineBlowUp I

The chart of a ∈ I [Hau14, Theorem 4.19]; [TSPA, Tag 0804]: the open immersion Spec R[I/a] ⟶ affineBlowUp I — Mathlib's chart Proj.awayι of D₊(a t) composed with Spec of the chart ring isomorphism.

Equations

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

instance AlgebraicGeometry.affineBlowUp.isOpenImmersion_chart {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : IsOpenImmersion (chart I a)

The charts are open immersions.

theorem AlgebraicGeometry.affineBlowUp.opensRange_chart {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : Scheme.Hom.opensRange (chart I a) = Proj.basicOpen (reesAlgebra.grading I) ((reesAlgebra.degreeOne I) a)

The image of the chart of a is the basic open D₊(a t) of Proj.

theorem AlgebraicGeometry.affineBlowUp.exists_mem_opensRange_chart {R : Type u} [CommRing R] (I : Ideal R) (x : ↥(affineBlowUp I)) : ∃ (a : ↥I), x ∈ Scheme.Hom.opensRange (chart I a)

Every point of the affine blow-up lies in the chart of some a ∈ I: the D₊(a t) cover Proj because the a t generate the irrelevant ideal (reesAlgebra.irrelevant_le_span_degreeOne; Mathlib's Proj.iSup_basicOpen_eq_top).

noncomputable def AlgebraicGeometry.affineBlowUp.affineOpenCover {R : Type u} [CommRing R] (I : Ideal R) : (affineBlowUp I).AffineOpenCover

The chart cover: the charts Spec R[I/a], a ∈ I, form an affine open cover of the affine blow-up [TSPA, Tag 0804].

Equations

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

theorem AlgebraicGeometry.affineBlowUp.iSup_opensRange_chart {R : Type u} [CommRing R] (I : Ideal R) : ⨆ (a : ↥I), Scheme.Hom.opensRange (chart I a) = ⊤

The charts cover.

theorem AlgebraicGeometry.affineBlowUp.exists_mem_opensRange_chart_of_span_eq {R : Type u} [CommRing R] (I : Ideal R) (s : Set R) (hs : Ideal.span s = I) (x : ↥(affineBlowUp I)) : ∃ (y : ↑s), x ∈ Scheme.Hom.opensRange (chart I ⟨↑y, ⋯⟩)

Every point lies in the chart of some element of a generating set s of I (Hauser's charts of the generators g₁, …, g_k [Hau14, Theorem 4.19]).

noncomputable def AlgebraicGeometry.affineBlowUp.affineOpenCoverOfSpan {R : Type u} [CommRing R] (I : Ideal R) (s : Set R) (hs : Ideal.span s = I) : (affineBlowUp I).AffineOpenCover

The charts of a generating set s of I form an affine open cover; for I = 0 the empty family is allowed.

Equations

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

theorem AlgebraicGeometry.affineBlowUp.iSup_opensRange_chart_of_span_eq {R : Type u} [CommRing R] (I : Ideal R) (s : Set R) (hs : Ideal.span s = I) : ⨆ (y : ↑s), Scheme.Hom.opensRange (chart I ⟨↑y, ⋯⟩) = ⊤

The charts of a generating set cover.

theorem AlgebraicGeometry.affineBlowUp.isEmpty_bot {R : Type u} [CommRing R] : IsEmpty ↥(affineBlowUp ⊥)

The affine blow-up along I = 0 is empty — the empty generating set gives the empty cover. Blowing up the zero ideal gives the empty scheme [TSPA, Tag 02OS]; the Rees algebra of the zero ideal is R in degree zero alone [Hau14, Definition 4.6].

theorem AlgebraicGeometry.affineBlowUp.chart_π {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : CategoryTheory.CategoryStruct.comp (chart I a) (π I) = Spec.map (CommRingCat.ofHom (algebraMap R ↥(affineBlowUpAlgebra I ↑a)))

Over the base, the chart of a is Spec of R → R[I/a] — Hauser's chart expression of the blow-up map [Hau14, Theorem 4.19] — by Proj.awayι_toSpecZero and the constant-map compatibility of the chart ring isomorphism (reesAlgebra.chartRingEquiv_fromZeroRingHom).

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.ratio {R : Type u} [CommRing R] (I : Ideal R) (a b : ↥I) : ↥(affineBlowUpAlgebra I ↑a)

The fraction b/a, a, b ∈ I, as an element of R[I/a].

Equations

• AlgebraicGeometry.affineBlowUpAlgebra.ratio I a b = ⟨AlgebraicGeometry.awayFrac (↑a) 1 ↑b, ⋯⟩

theorem reesAlgebra.chartRingEquiv_isLocalizationElem {R : Type u} [CommRing R] (I : Ideal R) (a b : ↥I) : (chartRingEquiv a) (HomogeneousLocalization.Away.isLocalizationElem ⋯ ⋯) = AlgebraicGeometry.affineBlowUpAlgebra.ratio I a b

Mathlib's localization element bt/at of (R̃_{at})₀ corresponds to b/a ∈ R[I/a].

theorem AlgebraicGeometry.affineBlowUp.chart_preimage_chart {R : Type u} [CommRing R] (I : Ideal R) (a b : ↥I) : (TopologicalSpace.Opens.map (chart I a).base).obj (Scheme.Hom.opensRange (chart I b)) = PrimeSpectrum.basicOpen (affineBlowUpAlgebra.ratio I a b)

Chart overlaps: inside the chart of a, the chart of b is the basic open D(b/a) ⊆ Spec R[I/a] — the identity D₊(f) ∩ D₊(g) = D₊(fg) of Proj for f = at, g = bt; this is how the charts are glued in [Hau14, Definition 4.13].