Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Projective spectrum of a graded ring #

The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal. It is naturally endowed with a topology: the Zariski topology.

Notation #

Main definitions #

theorem ProjectiveSpectrum.ext {R : Type u_1} {A : Type u_2} :
โˆ€ {inst : CommSemiring R} {inst_1 : CommRing A} {inst_2 : Algebra R A} {๐’œ : โ„• โ†’ Submodule R A} {inst_3 : GradedAlgebra ๐’œ} (x y : ProjectiveSpectrum ๐’œ), x.asHomogeneousIdeal = y.asHomogeneousIdeal โ†’ x = y
theorem ProjectiveSpectrum.ext_iff {R : Type u_1} {A : Type u_2} :
โˆ€ {inst : CommSemiring R} {inst_1 : CommRing A} {inst_2 : Algebra R A} {๐’œ : โ„• โ†’ Submodule R A} {inst_3 : GradedAlgebra ๐’œ} (x y : ProjectiveSpectrum ๐’œ), x = y โ†” x.asHomogeneousIdeal = y.asHomogeneousIdeal
structure ProjectiveSpectrum {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
Type u_2

The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal.

Instances For
    theorem ProjectiveSpectrum.isPrime {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (self : ProjectiveSpectrum ๐’œ) :
    self.asHomogeneousIdeal.toIdeal.IsPrime
    theorem ProjectiveSpectrum.not_irrelevant_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (self : ProjectiveSpectrum ๐’œ) :
    ยฌHomogeneousIdeal.irrelevant ๐’œ โ‰ค self.asHomogeneousIdeal
    def ProjectiveSpectrum.zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) :

    The zero locus of a set s of elements of a commutative ring A is the set of all relevant homogeneous prime ideals of the ring that contain the set s.

    An element f of A can be thought of as a dependent function on the projective spectrum of ๐’œ. At a point x (a homogeneous prime ideal) the function (i.e., element) f takes values in the quotient ring A modulo the prime ideal x. In this manner, zeroLocus s is exactly the subset of ProjectiveSpectrum ๐’œ where all "functions" in s vanish simultaneously.

    Equations
    Instances For
      @[simp]
      theorem ProjectiveSpectrum.mem_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (s : Set A) :
      x โˆˆ ProjectiveSpectrum.zeroLocus ๐’œ s โ†” s โŠ† โ†‘x.asHomogeneousIdeal
      @[simp]
      theorem ProjectiveSpectrum.zeroLocus_span {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) :
      def ProjectiveSpectrum.vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) :

      The vanishing ideal of a set t of points of the projective spectrum of a commutative ring R is the intersection of all the relevant homogeneous prime ideals in the set t.

      An element f of A can be thought of as a dependent function on the projective spectrum of ๐’œ. At a point x (a homogeneous prime ideal) the function (i.e., element) f takes values in the quotient ring A modulo the prime ideal x. In this manner, vanishingIdeal t is exactly the ideal of A consisting of all "functions" that vanish on all of t.

      Equations
      Instances For
        theorem ProjectiveSpectrum.coe_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) :
        โ†‘(ProjectiveSpectrum.vanishingIdeal t) = {f : A | โˆ€ x โˆˆ t, f โˆˆ x.asHomogeneousIdeal}
        theorem ProjectiveSpectrum.mem_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) (f : A) :
        f โˆˆ ProjectiveSpectrum.vanishingIdeal t โ†” โˆ€ x โˆˆ t, f โˆˆ x.asHomogeneousIdeal
        @[simp]
        theorem ProjectiveSpectrum.vanishingIdeal_singleton {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) :
        ProjectiveSpectrum.vanishingIdeal {x} = x.asHomogeneousIdeal
        theorem ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (t : Set (ProjectiveSpectrum ๐’œ)) (I : Ideal A) :
        theorem ProjectiveSpectrum.gc_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        GaloisConnection (fun (I : Ideal A) => ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I) fun (t : (Set (ProjectiveSpectrum ๐’œ))แต’แตˆ) => (ProjectiveSpectrum.vanishingIdeal t).toIdeal

        zeroLocus and vanishingIdeal form a galois connection.

        theorem ProjectiveSpectrum.gc_set {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

        zeroLocus and vanishingIdeal form a galois connection.

        theorem ProjectiveSpectrum.gc_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        theorem ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) :
        theorem ProjectiveSpectrum.zeroLocus_anti_mono {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : Set A} {t : Set A} (h : s โŠ† t) :
        theorem ProjectiveSpectrum.zeroLocus_anti_mono_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : Ideal A} {t : Ideal A} (h : s โ‰ค t) :
        theorem ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : HomogeneousIdeal ๐’œ} {t : HomogeneousIdeal ๐’œ} (h : s โ‰ค t) :
        theorem ProjectiveSpectrum.zeroLocus_bot {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘โŠฅ = Set.univ
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_singleton_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        ProjectiveSpectrum.zeroLocus ๐’œ {0} = Set.univ
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_empty {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        theorem ProjectiveSpectrum.zeroLocus_empty_of_one_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {s : Set A} (h : 1 โˆˆ s) :
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_singleton_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_univ {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        theorem ProjectiveSpectrum.zeroLocus_sup_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) (J : Ideal A) :
        theorem ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : HomogeneousIdeal ๐’œ) (J : HomogeneousIdeal ๐’œ) :
        theorem ProjectiveSpectrum.zeroLocus_union {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) (s' : Set A) :
        theorem ProjectiveSpectrum.zeroLocus_iSup_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (I : ฮณ โ†’ Ideal A) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(โจ† (i : ฮณ), I i) = โ‹‚ (i : ฮณ), ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I i)
        theorem ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (I : ฮณ โ†’ HomogeneousIdeal ๐’œ) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(โจ† (i : ฮณ), I i) = โ‹‚ (i : ฮณ), ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I i)
        theorem ProjectiveSpectrum.zeroLocus_iUnion {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (s : ฮณ โ†’ Set A) :
        ProjectiveSpectrum.zeroLocus ๐’œ (โ‹ƒ (i : ฮณ), s i) = โ‹‚ (i : ฮณ), ProjectiveSpectrum.zeroLocus ๐’œ (s i)
        theorem ProjectiveSpectrum.zeroLocus_bUnion {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set (Set A)) :
        ProjectiveSpectrum.zeroLocus ๐’œ (โ‹ƒ s' โˆˆ s, s') = โ‹‚ s' โˆˆ s, ProjectiveSpectrum.zeroLocus ๐’œ s'
        theorem ProjectiveSpectrum.vanishingIdeal_iUnion {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {ฮณ : Sort u_3} (t : ฮณ โ†’ Set (ProjectiveSpectrum ๐’œ)) :
        ProjectiveSpectrum.vanishingIdeal (โ‹ƒ (i : ฮณ), t i) = โจ… (i : ฮณ), ProjectiveSpectrum.vanishingIdeal (t i)
        theorem ProjectiveSpectrum.zeroLocus_inf {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) (J : Ideal A) :
        theorem ProjectiveSpectrum.union_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) (s' : Set A) :
        theorem ProjectiveSpectrum.zeroLocus_mul_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : Ideal A) (J : Ideal A) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I * J) = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โˆช ProjectiveSpectrum.zeroLocus ๐’œ โ†‘J
        theorem ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (I : HomogeneousIdeal ๐’œ) (J : HomogeneousIdeal ๐’œ) :
        ProjectiveSpectrum.zeroLocus ๐’œ โ†‘(I * J) = ProjectiveSpectrum.zeroLocus ๐’œ โ†‘I โˆช ProjectiveSpectrum.zeroLocus ๐’œ โ†‘J
        theorem ProjectiveSpectrum.zeroLocus_singleton_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_singleton_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (n : โ„•) (hn : 0 < n) :
        theorem ProjectiveSpectrum.mem_compl_zeroLocus_iff_not_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {f : A} {I : ProjectiveSpectrum ๐’œ} :
        I โˆˆ (ProjectiveSpectrum.zeroLocus ๐’œ {f})แถœ โ†” f โˆ‰ I.asHomogeneousIdeal
        instance ProjectiveSpectrum.zariskiTopology {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

        The Zariski topology on the prime spectrum of a commutative ring is defined via the closed sets of the topology: they are exactly those sets that are the zero locus of a subset of the ring.

        Equations
        def ProjectiveSpectrum.top {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

        The underlying topology of Proj is the projective spectrum of graded ring A.

        Equations
        Instances For
          theorem ProjectiveSpectrum.isOpen_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : Set (ProjectiveSpectrum ๐’œ)) :
          IsOpen U โ†” โˆƒ (s : Set A), Uแถœ = ProjectiveSpectrum.zeroLocus ๐’œ s
          theorem ProjectiveSpectrum.isClosed_iff_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (Z : Set (ProjectiveSpectrum ๐’œ)) :
          IsClosed Z โ†” โˆƒ (s : Set A), Z = ProjectiveSpectrum.zeroLocus ๐’œ s
          theorem ProjectiveSpectrum.isClosed_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (s : Set A) :
          def ProjectiveSpectrum.basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (r : A) :

          basicOpen r is the open subset containing all prime ideals not containing r.

          Equations
          Instances For
            @[simp]
            theorem ProjectiveSpectrum.mem_basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (x : ProjectiveSpectrum ๐’œ) :
            x โˆˆ ProjectiveSpectrum.basicOpen ๐’œ f โ†” f โˆ‰ x.asHomogeneousIdeal
            theorem ProjectiveSpectrum.mem_coe_basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (x : ProjectiveSpectrum ๐’œ) :
            x โˆˆ โ†‘(ProjectiveSpectrum.basicOpen ๐’œ f) โ†” f โˆ‰ x.asHomogeneousIdeal
            theorem ProjectiveSpectrum.isOpen_basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {a : A} :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (r : A) :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            theorem ProjectiveSpectrum.basicOpen_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
            theorem ProjectiveSpectrum.basicOpen_mul_le_left {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
            theorem ProjectiveSpectrum.basicOpen_mul_le_right {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (g : A) :
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) (n : โ„•) (hn : 0 < n) :
            theorem ProjectiveSpectrum.basicOpen_eq_union_of_projection {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (f : A) :
            ProjectiveSpectrum.basicOpen ๐’œ f = โจ† (i : โ„•), ProjectiveSpectrum.basicOpen ๐’œ ((GradedAlgebra.proj ๐’œ i) f)
            theorem ProjectiveSpectrum.isTopologicalBasis_basic_opens {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

            The specialization order #

            We endow ProjectiveSpectrum ๐’œ with a partial order, where x โ‰ค y if and only if y โˆˆ closure {x}.

            instance ProjectiveSpectrum.instPartialOrder {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            Equations
            @[simp]
            theorem ProjectiveSpectrum.as_ideal_le_as_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (y : ProjectiveSpectrum ๐’œ) :
            x.asHomogeneousIdeal โ‰ค y.asHomogeneousIdeal โ†” x โ‰ค y
            @[simp]
            theorem ProjectiveSpectrum.as_ideal_lt_as_ideal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (y : ProjectiveSpectrum ๐’œ) :
            x.asHomogeneousIdeal < y.asHomogeneousIdeal โ†” x < y
            theorem ProjectiveSpectrum.le_iff_mem_closure {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : ProjectiveSpectrum ๐’œ) (y : ProjectiveSpectrum ๐’œ) :