The exceptional ideal of the affine blow-up on its charts

For an ideal I of a commutative ring R, the exceptional ideal of the affine blow-up B = affineBlowUp I = Proj Rees(I) is the ideal sheaf I · 𝒪_B, the inverse image (IdealSheafData.comap) of the ideal sheaf of I on Spec R under the blow-up map π: the ideal of the exceptional divisor E = π⁻¹(Z) [Hau14, Definitions 4.4 and 4.7]; [TSPA, Tag 02OS]; [Kol07, Notation 19].

On the chart of a ∈ I, affineBlowUp.chart a ≫ π = Spec (R → R[I/a]) (affineBlowUp.chart_π), so the inverse image of I on the chart is the ideal sheaf of I·R[I/a] (the affine computation comap_ofIdealTop_Spec_map), which is a·R[I/a] (affineBlowUpAlgebra.map_algebraMap_eq_span_singleton) with a a nonzerodivisor of R[I/a] (affineBlowUpAlgebra.algebraMap_mem_nonZeroDivisors). Since the charts cover B, the exceptional ideal is invertible in the sense of IdealSheafData.IsInvertible (locally, on an affine open, principal with a nonzerodivisor generator): the exceptional divisor is an effective Cartier divisor [TSPA, Tag 02OS].

• affineBlowUp.exceptionalIdeal I : (affineBlowUp I).IdealSheafData — the exceptional ideal.
• affineBlowUp.comap_exceptionalIdeal_chart — its inverse image on the chart of a is the ideal sheaf of (a) ⊆ R[I/a].
• affineBlowUp.ideal_comap_exceptionalIdeal_chart_top, affineBlowUp.chartGenerator_mem_nonZeroDivisors — on Spec R[I/a] the exceptional ideal is generated by the image of a, a nonzerodivisor.
• affineBlowUp.exists_generator_exceptionalIdeal_opensRange_chart — the same on the affine open U_a ⊆ B, the image of the chart (transport along Scheme.Hom.appIso).
• affineBlowUp.isInvertible_exceptionalIdeal — the exceptional ideal is invertible.

The ideal sheaf of I on Spec R is written ofIdealTop (I.map (Scheme.ΓSpecIso (.of R)).inv.hom) (sections transported by ΓSpecIso), as throughout Hironaka.BlowUp.

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

The exceptional ideal I · 𝒪_B of the affine blow-up: the inverse image of the ideal sheaf of I on Spec R under the blow-up map — the ideal of the exceptional divisor E = π⁻¹(Z) [Hau14, Definition 4.4]; [TSPA, Tag 02OS]; [Kol07, Notation 19].

Equations

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

theorem AlgebraicGeometry.affineBlowUp.comap_exceptionalIdeal_chart {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : (exceptionalIdeal I).comap (chart I a) = Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧↥(affineBlowUpAlgebra I ↑a)).inv) (Ideal.span {(algebraMap R ↥(affineBlowUpAlgebra I ↑a)) ↑a}))

The inverse image of the exceptional ideal on the chart of a is the ideal sheaf of the principal ideal (a) of R[I/a] (the identity I A' = a A' on the chart Spec A' of [TSPA, Tag 02OS]) — from chart ≫ π = Spec (R → R[I/a]), the affine computation of the inverse image (comap_ofIdealTop_Spec_map) and I·R[I/a] = a·R[I/a].

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.affineBlowUp.chartGenerator {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : ↑((Spec ↧↥(affineBlowUpAlgebra I ↑a)).presheaf.obj (Opposite.op ⊤))

The generator of the exceptional ideal on the chart of a: the image of a in the global sections of Spec R[I/a].

Equations

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

theorem AlgebraicGeometry.affineBlowUp.ideal_comap_exceptionalIdeal_chart_top {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : ((exceptionalIdeal I).comap (chart I a)).ideal ⟨⊤, ⋯⟩ = Ideal.span {chartGenerator I a}

On Spec R[I/a] the exceptional ideal is the principal ideal generated by the image of a.

theorem AlgebraicGeometry.affineBlowUp.chartGenerator_mem_nonZeroDivisors {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : chartGenerator I a ∈ nonZeroDivisors ↑((Spec ↧↥(affineBlowUpAlgebra I ↑a)).presheaf.obj (Opposite.op ⊤))

The generator of the exceptional ideal on the chart of a is a nonzerodivisor (a is a unit of R_a ⊇ R[I/a]; [TSPA, Tag 02OS]).

theorem AlgebraicGeometry.affineBlowUp.exists_generator_exceptionalIdeal_image_chart {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) (W : (affineBlowUp I).Opens) (hW : IsAffineOpen W) (hWeq : W = (Scheme.Hom.opensFunctor (chart I a)).obj ⊤) : ∃ f ∈ nonZeroDivisors ↑((affineBlowUp I).presheaf.obj (Opposite.op W)), (exceptionalIdeal I).ideal ⟨W, hW⟩ = Ideal.span {f}

On the affine open U_a = chart a ''ᵁ ⊤ ⊆ B, the exceptional ideal is generated by a nonzerodivisor (the image of a, transported along the isomorphism Γ(B, U_a) ≅ Γ(Spec R[I/a], ⊤) of the open immersion).

theorem AlgebraicGeometry.affineBlowUp.exists_generator_exceptionalIdeal_opensRange_chart {R : Type u} [CommRing R] (I : Ideal R) (a : ↥I) : ∃ f ∈ nonZeroDivisors ↑((affineBlowUp I).presheaf.obj (Opposite.op (Scheme.Hom.opensRange (chart I a)))), (exceptionalIdeal I).ideal ⟨Scheme.Hom.opensRange (chart I a), ⋯⟩ = Ideal.span {f}

The same on the affine open U_a ⊆ B, the image of the chart of a.

theorem AlgebraicGeometry.affineBlowUp.isInvertible_exceptionalIdeal {R : Type u} [CommRing R] (I : Ideal R) : (exceptionalIdeal I).IsInvertible

The exceptional ideal of the affine blow-up is invertible — the exceptional divisor is an effective Cartier divisor [TSPA, Tag 02OS]; [Hau14, Definition 4.4]: every point lies in the chart of some a ∈ I, an affine open on which the exceptional ideal is generated by the nonzerodivisor a.