Documentation

TauCeti.AlgebraicGeometry.RelativeProj.Basic

The relative Proj of a graded quasi-coherent algebra #

Let A = ⨁ₙ Aₙ be a graded algebra on a scheme X whose homogeneous components are quasi-coherent. Over an affine open U of X, the sections of the homogeneous components form the graded Γ(X, U)-algebra ⨁ n, Γ(Aₙ, U) (CategoryTheory.CommMon.gCommRingSections), internally graded by its summands (CategoryTheory.CommMon.gradedSectionsGrading), and its projective spectrum is a scheme over Spec Γ(X, U) ≅ U. This file glues these schemes into the relative Proj

Proj_X(A) ⟶ X,

a scheme over X whose part over every affine open U is Proj (⨁ n, Γ(Aₙ, U)). Relative Proj is the construction behind blowups of quasi-coherent ideals and projective morphisms.

The gluing uses Mathlib's relative gluing along the affine opens of X (AlgebraicGeometry.Scheme.Cover.RelativeGluingData), whose transition maps are inclusions of basic opens D(f) ⊆ U. Its input is that these charts are compatible with restriction: for an affine open U and f ∈ Γ(X, U), restriction of sections exhibits ⨁ n, Γ(Aₙ, D(f)) as the base change of ⨁ n, Γ(Aₙ, U) along Γ(X, U) → Γ(X, D(f)), because both are localizations away from f (CategoryTheory.CommMon.isLocalization_gradedSections_basicOpen). As Proj commutes with base change (AlgebraicGeometry.Proj.isPullback_map_of_isBaseChange), the chart over D(f) is the pullback of the chart over U.

Main definitions #

Main results #

References #

source
theorem CategoryTheory.CommMon.irrelevant_le_map_restrictGradedSectionsGradedHom {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (hU : AlgebraicGeometry.IsAffineOpen U) (i : X.basicOpen f ⟶ U) :
HomogeneousIdeal.irrelevant (A.gradedSectionsGrading (X.basicOpen f)) ≤ HomogeneousIdeal.map (A.restrictGradedSectionsGradedHom i) (HomogeneousIdeal.irrelevant (A.gradedSectionsGrading U))

For an affine open U of X and f ∈ Γ(X, U), the irrelevant ideal of ⨁ n, Γ(Aₙ, D(f)) is contained in the ideal generated by the image of the irrelevant ideal of ⨁ n, Γ(Aₙ, U) under restriction of sections, so that Proj.map gives Proj (⨁ n, Γ(Aₙ, D(f))) ⟶ Proj (⨁ n, Γ(Aₙ, U)).

source
theorem CategoryTheory.CommMon.isPullback_proj_restrictGradedSections {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (hU : AlgebraicGeometry.IsAffineOpen U) (i : X.basicOpen f ⟶ U) :
IsPullback (AlgebraicGeometry.Proj.map (A.restrictGradedSectionsGradedHom i) ⋯) (AlgebraicGeometry.Proj.toSpecCoeff (A.gradedSectionsGrading (X.basicOpen f))) (AlgebraicGeometry.Proj.toSpecCoeff (A.gradedSectionsGrading U)) (AlgebraicGeometry.Spec.map (X.presheaf.map i.op))

The charts of the relative Proj are compatible with restriction. For an affine open U of X and f ∈ Γ(X, U), the square

Proj (⨁ n, Γ(Aₙ, D(f))) ⟶ Proj (⨁ n, Γ(Aₙ, U)), Spec Γ(X, D(f)) ⟶ Spec Γ(X, U)

formed by restriction of sections and the coefficient projections is cartesian.

source
theorem CategoryTheory.CommMon.proj_map_restrictGradedSections_preimage_basicOpen_eq_top {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (hU : AlgebraicGeometry.IsAffineOpen U) (i : X.basicOpen f ⟶ U) :
(TopologicalSpace.Opens.map (AlgebraicGeometry.Proj.map (A.restrictGradedSectionsGradedHom i) ⋯).base).obj (AlgebraicGeometry.Proj.basicOpen (A.gradedSectionsGrading U) ((algebraMap (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))) f)) = ⊤

The chart Proj (⨁ n, Γ(Aₙ, D(f))) of the relative Proj maps into the locus of the chart Proj (⨁ n, Γ(Aₙ, U)) where the image of f in degree zero is invertible.

source
theorem CategoryTheory.CommMon.irrelevant_le_map_restrictGradedSectionsGradedHom_toOpensFunctor {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] {U V : X.AffineZariskiSite} (i : U ⟶ V) :
HomogeneousIdeal.irrelevant (A.gradedSectionsGrading U.toOpens) ≤ HomogeneousIdeal.map (A.restrictGradedSectionsGradedHom ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).map i)) (HomogeneousIdeal.irrelevant (A.gradedSectionsGrading V.toOpens))

For an arrow i : U ⟶ V of the small affine Zariski site of X, the irrelevant ideal of ⨁ n, Γ(Aₙ, U) is contained in the ideal generated by the image of the irrelevant ideal of ⨁ n, Γ(Aₙ, V) under restriction of sections along i, so that Proj.map applies. This holds because U is a basic open of the affine open V.

source
noncomputable def CategoryTheory.CommMon.relativeProjFunctor {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
Functor X.AffineZariskiSite AlgebraicGeometry.Scheme

The schemes Proj (⨁ n, Γ(Aₙ, U)) over the affine opens U of X, with the morphisms induced by restriction of sections to basic opens.

Instances For
    source
    noncomputable def CategoryTheory.CommMon.relativeProjToSpec {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
    A.relativeProjFunctor ⟶ (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).comp ((Functor.rightOp X.presheaf).comp AlgebraicGeometry.Scheme.Spec)

    The coefficient projections Proj (⨁ n, Γ(Aₙ, U)) ⟶ Spec Γ(X, U), natural in the affine open U.

    Instances For
      source
      theorem CategoryTheory.CommMon.equifibered_relativeProjToSpec {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
      NatTrans.Equifibered A.relativeProjToSpec

      The coefficient projections of the charts of the relative Proj form an equifibered natural transformation: every naturality square is cartesian.

      source
      noncomputable def CategoryTheory.CommMon.relativeProjGluingData {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
      AlgebraicGeometry.Scheme.Cover.RelativeGluingData (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X)

      The relative gluing datum of the relative Proj of A: the schemes Proj (⨁ n, Γ(Aₙ, U)) over the affine opens U of X.

      Instances For
        source
        theorem CategoryTheory.CommMon.relativeProjGluingData_functor_map {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] {U V : X.AffineZariskiSite} (i : U ⟶ V) :
        A.relativeProjGluingData.functor.map i = AlgebraicGeometry.Proj.map (A.restrictGradedSectionsGradedHom ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).map i)) ⋯

        The transition maps of the relative Proj gluing datum are the morphisms of projective spectra induced by restriction of sections.

        source
        theorem CategoryTheory.CommMon.relativeProjGluingData_natTrans_app {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (U : X.AffineZariskiSite) :
        A.relativeProjGluingData.natTrans.app U = CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecCoeff (A.gradedSectionsGrading U.toOpens)) ⋯.isoSpec.inv

        The structure morphisms of the relative Proj gluing datum are the coefficient projections Proj (⨁ n, Γ(Aₙ, U)) ⟶ Spec Γ(X, U) followed by Spec Γ(X, U) ≅ U.

        source
        instance CategoryTheory.CommMon.isLocallyDirected_relativeProjGluingData {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
        (A.relativeProjGluingData.functor.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected

        The gluing diagram of the relative Proj is locally directed.

        source
        noncomputable def CategoryTheory.CommMon.relativeProj {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
        AlgebraicGeometry.Scheme

        The relative Proj Proj_X(A) of a graded algebra A on X with quasi-coherent homogeneous components, glued from the schemes Proj (⨁ n, Γ(Aₙ, U)) over the affine opens U of X.

        Instances For
          source
          noncomputable def CategoryTheory.CommMon.relativeProjToBase {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
          A.relativeProj ⟶ X

          The structure morphism Proj_X(A) ⟶ X of the relative Proj.

          Instances For
            source
            noncomputable def CategoryTheory.CommMon.relativeProjCover {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] :
            A.relativeProj.OpenCover

            The open cover of the relative Proj by the schemes Proj (⨁ n, Γ(Aₙ, U)) over the affine opens U of X.

            Instances For
              source
              instance CategoryTheory.CommMon.isOpenImmersion_relativeProjCover_f {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (U : X.AffineZariskiSite) :
              AlgebraicGeometry.IsOpenImmersion (A.relativeProjCover.f U)

              The charts of the relative Proj are open immersions.

              source
              theorem CategoryTheory.CommMon.relativeProjCover_X {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (U : X.AffineZariskiSite) :
              A.relativeProjCover.X U = AlgebraicGeometry.Proj (A.gradedSectionsGrading U.toOpens)

              The chart of the relative Proj over an affine open U is Proj (⨁ n, Γ(Aₙ, U)).

              source
              theorem CategoryTheory.CommMon.relativeProjCover_f_relativeProjToBase {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (U : X.AffineZariskiSite) :
              CategoryStruct.comp (A.relativeProjCover.f U) A.relativeProjToBase = CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecCoeff (A.gradedSectionsGrading U.toOpens)) ⋯.fromSpec

              Over an affine open U, the structure morphism of the relative Proj is the coefficient projection Proj (⨁ n, Γ(Aₙ, U)) ⟶ Spec Γ(X, U) followed by the chart Spec Γ(X, U) ⟶ X.

              source
              theorem CategoryTheory.CommMon.relativeProjCover_f_relativeProjToBase_assoc {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (U : X.AffineZariskiSite) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
              CategoryStruct.comp (A.relativeProjCover.f U) (CategoryStruct.comp A.relativeProjToBase h) = CategoryStruct.comp (CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecCoeff (A.gradedSectionsGrading U.toOpens)) ⋯.fromSpec) h

              Over an affine open U, the structure morphism of the relative Proj is the coefficient projection Proj (⨁ n, Γ(Aₙ, U)) ⟶ Spec Γ(X, U) followed by the chart Spec Γ(X, U) ⟶ X.

              source
              theorem CategoryTheory.CommMon.relativeProjToBase_preimage {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (U : X.AffineZariskiSite) :
              (TopologicalSpace.Opens.map A.relativeProjToBase.base).obj U.toOpens = AlgebraicGeometry.Scheme.Hom.opensRange (A.relativeProjCover.f U)

              The preimage of an affine open U under the structure morphism of the relative Proj is the image of the chart Proj (⨁ n, Γ(Aₙ, U)).

              source
              theorem CategoryTheory.CommMon.isPullback_relativeProjCover {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)] (U : X.AffineZariskiSite) :
              IsPullback (CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecCoeff (A.gradedSectionsGrading U.toOpens)) ⋯.isoSpec.inv) (A.relativeProjCover.f U) U.toOpens.ι A.relativeProjToBase

              Over an affine open U of X, the relative Proj is Proj (⨁ n, Γ(Aₙ, U)): the chart of the relative Proj over U is the base change of its structure morphism along U ⟶ X.