Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Proj as a scheme #

This file is to prove that Proj is a scheme.

Notation #

Implementation #

In AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean, we have given Proj a structure sheaf so that Proj is a locally ringed space. In this file we will prove that Proj equipped with this structure sheaf is a scheme. We achieve this by using an affine cover by basic open sets in Proj, more specifically:

  1. We prove that Proj can be covered by basic open sets at homogeneous element of positive degree.
  2. We prove that for any homogeneous element f : A of positive degree m, Proj.T | (pbo f) is homeomorphic to Spec.T A⁰_f:
  1. Then we construct a morphism of locally ringed spaces α : Proj| (pbo f) ⟶ Spec.T A⁰_f as the following: by the Gamma-Spec adjunction, it is sufficient to construct a ring map A⁰_f → Γ(Proj, pbo f) from the ring of homogeneous localization of A away from f to the local sections of structure sheaf of projective spectrum on the basic open set around f. The map A⁰_f → Γ(Proj, pbo f) is constructed in awayToΓ and is defined by sending s ∈ A⁰_f to the section x ↦ s on pbo f.

Main Definitions and Statements #

For a homogeneous element f of degree m

If we further assume m is positive

Finally,

Reference #

Proj restrict to some open set

Equations
Instances For
    def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} (x : ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ).toTopCat) :

    For any x in Proj| (pbo f), the corresponding ideal in Spec A⁰_f. This fact that this ideal is prime is proven in TopComponent.Forward.toFun

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] (f : A) (x : ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ).toPresheafedSpace) :

      The function between the basic open set D(f) in Proj to the corresponding basic open set in Spec A⁰_f. This is bundled into a continuous map in TopComponent.forward.

      Equations
      Instances For
        def AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] (f : A) :

        The continuous function from the basic open set D(f) in Proj to the corresponding basic open set in Spec A⁰_f.

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (q : (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :
              Set A

              The function from Spec A⁰_f to Proj|D(f) is defined by q ↦ {a | aᵢᵐ/fⁱ ∈ q}, i.e. sending q a prime ideal in A⁰_f to the homogeneous prime relevant ideal containing only and all the elements a : A such that for every i, the degree 0 element formed by dividing the m-th power of the i-th projection of a by the i-th power of the degree-m homogeneous element f, lies in q.

              The set {a | aᵢᵐ/fⁱ ∈ q}

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (q : (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) :
                a AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ∀ (i : ), HomogeneousLocalization.mk { deg := m * i, num := (GradedAlgebra.proj 𝒜 i) a ^ m, , den := f ^ i, , den_mem := } q.asIdeal
                theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) {n : } (hn : a 𝒜 n) :
                a AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q HomogeneousLocalization.mk { deg := m * n, num := a ^ m, , den := f ^ n, , den_mem := } q.asIdeal
                theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) {n : } (hn : a 𝒜 (n * m)) :
                a AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q HomogeneousLocalization.mk { deg := m * n, num := a, , den := f ^ n, , den_mem := } q.asIdeal
                def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :

                For a prime ideal q in A⁰_f, the set {a | aᵢᵐ/fⁱ ∈ q} as an ideal.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :

                  For a prime ideal q in A⁰_f, the set {a | aᵢᵐ/fⁱ ∈ q} as a homogeneous ideal.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
                    (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ).toPresheafedSpace

                    The function Spec A⁰_f → Proj|D(f) sending q to {a | aᵢᵐ/fⁱ ∈ q}.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[deprecated AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec]

                      Alias of AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec.

                      theorem AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (x : ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ).toPresheafedSpace) :
                      theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
                      theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
                      theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
                      theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (a : A) (i : ) :
                      (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f) '' (Subtype.val ⁻¹' (ProjectiveSpectrum.basicOpen 𝒜 (((DirectSum.decompose 𝒜) a) i))) = (PrimeSpectrum.basicOpen (HomogeneousLocalization.mk { deg := m * i, num := (((DirectSum.decompose 𝒜) a) i) ^ m, , den := f ^ i, , den_mem := })).carrier
                      def AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :

                      The continuous function Spec A⁰_f → Proj|D(f) sending q to {a | aᵢᵐ/fⁱ ∈ q} where m is the degree of f

                      Equations
                      Instances For
                        def AlgebraicGeometry.projIsoSpecTopComponent {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :

                        The homeomorphism Proj|D(f) ≅ Spec A⁰_f defined by

                        • φ : Proj|D(f) ⟶ Spec A⁰_f by sending x to A⁰_f ∩ span {g / 1 | g ∈ x}
                        • ψ : Spec A⁰_f ⟶ Proj|D(f) by sending q to {a | aᵢᵐ/fⁱ ∈ q}.
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The ring map from A⁰_ f to the local sections of the structure sheaf of the projective spectrum of A on the basic open set D(f) defined by sending s ∈ A⁰_f to the section x ↦ s on D(f).

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

                            The ring map from A⁰_ f to the global sections of the structure sheaf of the projective spectrum of A restricted to the basic open set D(f).

                            Mathematically, the map is the same as awayToSection.

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

                              The morphism of locally ringed space from Proj|D(f) to Spec A⁰_f induced by the ring map A⁰_ f → Γ(Proj, D(f)) under the gamma spec adjunction.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
                                theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} (x : ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ).toTopCat) (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)) :
                                HomogeneousLocalization.mk z ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x).asIdeal z.num (x).asHomogeneousIdeal
                                theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] (f : A) (x : (ProjectiveSpectrum.basicOpen 𝒜 f)) {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
                                IsLocalization ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x).asIdeal.primeCompl (HomogeneousLocalization.AtPrime 𝒜 (x).asHomogeneousIdeal.toIdeal)

                                If x is a point in the basic open set D(f) where f is a homogeneous element of positive degree, then the homogeneously localized ring A⁰ₓ has the universal property of the localization of A⁰_f at φ(x) where φ : Proj|D(f) ⟶ Spec A⁰_f is the morphism of locally ringed space constructed as above.

                                def AlgebraicGeometry.ProjectiveSpectrum.Proj.specStalkEquiv {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] (f : A) (x : (ProjectiveSpectrum.basicOpen 𝒜 f)) {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :

                                For an element f ∈ A with positive degree and a homogeneous ideal in D(f), we have that the stalk of Spec A⁰_ f at y is isomorphic to A⁰ₓ where y is the point in Proj corresponding to x.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
                                  def AlgebraicGeometry.projIsoSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :

                                  If f ∈ A is a homogeneous element of positive degree, then the projective spectrum restricted to D(f) as a locally ringed space is isomorphic to Spec A⁰_f.

                                  Equations
                                  Instances For
                                    def AlgebraicGeometry.Proj {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] :

                                    This is the scheme Proj(A) for any -graded ring A.

                                    Equations
                                    Instances For