Documentation

TauCeti.AlgebraicGeometry.Blowup.IdealSheaf

The blowup of a scheme along an ideal sheaf #

Let I ⊆ 𝒪_X be an ideal sheaf on a scheme X. The blowup of X along the closed subscheme V(I) is the relative Proj of the Rees algebra ⨁ₙ Iⁿ of I (AlgebraicGeometry.Scheme.IdealSheafData.reesAlgebra),

Bl_I X = Proj_X(⨁ₙ Iⁿ) ⟶ X.

Over an affine open U of X, the graded ring of sections ⨁ n, Γ(Iⁿ, U) of the Rees algebra is the Rees algebra Γ(X, U)[I(U)t] of the ideal I(U) ⊆ Γ(X, U), with its grading by the power of t (AlgebraicGeometry.Scheme.IdealSheafData.reesAlgebraSectionsEquiv). Consequently the part of the blowup over U is the blowup Proj Γ(X, U)[I(U)t] of the affine scheme U ≅ Spec Γ(X, U) along V(I(U)), whose affine charts, universal property, behaviour away from the centre and base change are developed in the other files of this directory. When I is of finite type, the Rees algebras Γ(X, U)[I(U)t] are finitely generated, and the blowup is proper over X.

Main definitions #

Main results #

References #

The graded isomorphism over an affine open #

The blowup #

source
@[reducible, inline]
noncomputable abbrev AlgebraicGeometry.Scheme.IdealSheafData.blowup {X : Scheme} (I : X.IdealSheafData) :
Scheme

The blowup Bl_I X of a scheme X along the closed subscheme V(I) cut out by an ideal sheaf I: the relative Proj of the Rees algebra ⨁ₙ Iⁿ of I. It is an abbreviation, so that the API of the relative Proj applies to it directly.

Instances For
    source
    @[reducible, inline]
    noncomputable abbrev AlgebraicGeometry.Scheme.IdealSheafData.blowupToBase {X : Scheme} (I : X.IdealSheafData) :
    I.blowup ⟶ X

    The structure morphism Bl_I X ⟶ X of the blowup of X along V(I).

    Instances For
      source
      noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowupChart {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) :
      Proj (reesAlgebra.grade (I.ideal ⟨U, hU⟩)) ⟶ I.blowup

      The affine chart of the blowup over an affine open U of X: the open immersion of the blowup Proj Γ(X, U)[I(U)t] of Spec Γ(X, U) along V(I(U)) into the blowup of X along V(I). Its image is the preimage of U (isPullback_blowupChart).

      Instances For
        source
        instance AlgebraicGeometry.Scheme.IdealSheafData.instIsOpenImmersionBlowupChart {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) :
        IsOpenImmersion (I.blowupChart hU)
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupChart_blowupToBase {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) :
        CategoryTheory.CategoryStruct.comp (I.blowupChart hU) I.blowupToBase = CategoryTheory.CategoryStruct.comp (Proj.toSpecCoeff (reesAlgebra.grade (I.ideal ⟨U, hU⟩))) hU.fromSpec

        The affine chart of the blowup over U lies over U: followed by the structure morphism of the blowup, it is the structure morphism Proj Γ(X, U)[I(U)t] ⟶ Spec Γ(X, U) followed by the inclusion Spec Γ(X, U) ≅ U ⟶ X.

        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupChart_blowupToBase_assoc {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) {Z : Scheme} (h : X ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (I.blowupChart hU) (CategoryTheory.CategoryStruct.comp I.blowupToBase h) = CategoryTheory.CategoryStruct.comp (Proj.toSpecCoeff (reesAlgebra.grade (I.ideal ⟨U, hU⟩))) (CategoryTheory.CategoryStruct.comp hU.fromSpec h)

        The affine chart of the blowup over U lies over U: followed by the structure morphism of the blowup, it is the structure morphism Proj Γ(X, U)[I(U)t] ⟶ Spec Γ(X, U) followed by the inclusion Spec Γ(X, U) ≅ U ⟶ X.

        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_blowupChart {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) :
        Hom.opensRange (I.blowupChart hU) = (TopologicalSpace.Opens.map I.blowupToBase.base).obj U

        The image of the affine chart of the blowup over U is the preimage of U.

        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.isPullback_blowupChart {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) :
        CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (Proj.toSpecCoeff (reesAlgebra.grade (I.ideal ⟨U, hU⟩))) hU.isoSpec.inv) (I.blowupChart hU) U.ι I.blowupToBase

        Over an affine open U of X, the blowup of X along V(I) is the blowup Proj Γ(X, U)[I(U)t] of U ≅ Spec Γ(X, U) along V(I(U)): the affine chart over U is the base change of the blowup along the inclusion U ⟶ X.

        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.isPullback_blowupChart_fromSpec {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) :
        CategoryTheory.IsPullback (Proj.toSpecCoeff (reesAlgebra.grade (I.ideal ⟨U, hU⟩))) (I.blowupChart hU) hU.fromSpec I.blowupToBase

        The affine chart of the blowup over U is the base change of the blowup along Spec Γ(X, U) ⟶ X: the form of isPullback_blowupChart over the spectrum of the sections.

        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.isProper_blowupToBase {X : Scheme} (I : X.IdealSheafData) (hI : ∀ (U : ↑X.affineOpens), (I.ideal U).FG) :
        IsProper I.blowupToBase

        The blowup along an ideal sheaf of finite type is proper. If the ideal I(U) is finitely generated for every affine open U of X, then Bl_I X ⟶ X is proper.

        source
        instance AlgebraicGeometry.Scheme.IdealSheafData.isProper_blowupToBase_of_isLocallyNoetherian {X : Scheme} (I : X.IdealSheafData) [IsLocallyNoetherian X] :
        IsProper I.blowupToBase

        The blowup of a locally noetherian scheme is proper. On a locally noetherian scheme every ideal sheaf is of finite type, so Bl_I X ⟶ X is proper for every ideal sheaf I.