Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Projective spectrum of a graded ring #

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

Notation #

Main definitions #

source
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 homogeneous ideals that are prime and do not contain the irrelevant ideal.

Instances For
    source
    theorem ProjectiveSpectrum.ext_iff {R : Type u_1} {A : Type u_2} {inst✝ : CommSemiring R} {inst✝¹ : CommRing A} {inst✝² : Algebra R A} {π’œ : β„• β†’ Submodule R A} {inst✝³ : GradedAlgebra π’œ} {x y : ProjectiveSpectrum π’œ} :
    x = y ↔ x.asHomogeneousIdeal = y.asHomogeneousIdeal
    source
    theorem ProjectiveSpectrum.ext {R : Type u_1} {A : Type u_2} {inst✝ : CommSemiring R} {inst✝¹ : CommRing A} {inst✝² : Algebra R A} {π’œ : β„• β†’ Submodule R A} {inst✝³ : GradedAlgebra π’œ} {x y : ProjectiveSpectrum π’œ} (asHomogeneousIdeal : x.asHomogeneousIdeal = y.asHomogeneousIdeal) :
    x = y
    source
    instance ProjectiveSpectrum.instIsPrimeToIdealNatSubmoduleAsHomogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (x : ProjectiveSpectrum π’œ) :
    x.asHomogeneousIdeal.toIdeal.IsPrime
    source
    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) :
    Set (ProjectiveSpectrum π’œ)

    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
      source
      @[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 ∈ zeroLocus π’œ s ↔ s βŠ† ↑x.asHomogeneousIdeal
      source
      @[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) :
      zeroLocus π’œ ↑(Ideal.span s) = zeroLocus π’œ s
      source
      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 π’œ)) :
      HomogeneousIdeal π’œ

      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
        source
        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 π’œ)) :
        ↑(vanishingIdeal t) = {f : A | βˆ€ x ∈ t, f ∈ x.asHomogeneousIdeal}
        source
        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 ∈ vanishingIdeal t ↔ βˆ€ x ∈ t, f ∈ x.asHomogeneousIdeal
        source
        @[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 π’œ) :
        vanishingIdeal {x} = x.asHomogeneousIdeal
        source
        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) :
        t βŠ† zeroLocus π’œ ↑I ↔ I ≀ (vanishingIdeal t).toIdeal
        source
        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) => zeroLocus π’œ ↑I) fun (t : (Set (ProjectiveSpectrum π’œ))α΅’α΅ˆ) => (vanishingIdeal t).toIdeal

        zeroLocus and vanishingIdeal form a galois connection.

        source
        theorem ProjectiveSpectrum.gc_set {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        GaloisConnection (fun (s : Set A) => zeroLocus π’œ s) fun (t : (Set (ProjectiveSpectrum π’œ))α΅’α΅ˆ) => ↑(vanishingIdeal t)

        zeroLocus and vanishingIdeal form a galois connection.

        source
        theorem ProjectiveSpectrum.gc_homogeneousIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        GaloisConnection (fun (I : HomogeneousIdeal π’œ) => zeroLocus π’œ ↑I) fun (t : (Set (ProjectiveSpectrum π’œ))α΅’α΅ˆ) => vanishingIdeal t
        source
        theorem ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (t : Set (ProjectiveSpectrum π’œ)) (s : Set A) :
        t βŠ† zeroLocus π’œ s ↔ s βŠ† ↑(vanishingIdeal t)
        source
        theorem ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (s : Set A) :
        s βŠ† ↑(vanishingIdeal (zeroLocus π’œ s))
        source
        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) :
        I ≀ (vanishingIdeal (zeroLocus π’œ ↑I)).toIdeal
        source
        theorem ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (I : HomogeneousIdeal π’œ) :
        I ≀ vanishingIdeal (zeroLocus π’œ ↑I)
        source
        theorem ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (t : Set (ProjectiveSpectrum π’œ)) :
        t βŠ† zeroLocus π’œ ↑(vanishingIdeal t)
        source
        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 t : Set A} (h : s βŠ† t) :
        zeroLocus π’œ t βŠ† zeroLocus π’œ s
        source
        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 t : Ideal A} (h : s ≀ t) :
        zeroLocus π’œ ↑t βŠ† zeroLocus π’œ ↑s
        source
        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 t : HomogeneousIdeal π’œ} (h : s ≀ t) :
        zeroLocus π’œ ↑t βŠ† zeroLocus π’œ ↑s
        source
        theorem ProjectiveSpectrum.vanishingIdeal_anti_mono {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] {s t : Set (ProjectiveSpectrum π’œ)} (h : s βŠ† t) :
        vanishingIdeal t ≀ vanishingIdeal s
        source
        theorem ProjectiveSpectrum.zeroLocus_bot {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        zeroLocus π’œ ↑βŠ₯ = Set.univ
        source
        @[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 π’œ] :
        zeroLocus π’œ {0} = Set.univ
        source
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_empty {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        zeroLocus π’œ βˆ… = Set.univ
        source
        @[simp]
        theorem ProjectiveSpectrum.vanishingIdeal_univ {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        vanishingIdeal βˆ… = ⊀
        source
        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) :
        zeroLocus π’œ s = βˆ…
        source
        @[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 π’œ] :
        zeroLocus π’œ {1} = βˆ…
        source
        @[simp]
        theorem ProjectiveSpectrum.zeroLocus_univ {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        zeroLocus π’œ Set.univ = βˆ…
        source
        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 J : Ideal A) :
        zeroLocus π’œ ↑(I βŠ” J) = zeroLocus π’œ ↑I ∩ zeroLocus π’œ ↑J
        source
        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 J : HomogeneousIdeal π’œ) :
        zeroLocus π’œ ↑(I βŠ” J) = zeroLocus π’œ ↑I ∩ zeroLocus π’œ ↑J
        source
        theorem ProjectiveSpectrum.zeroLocus_union {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (s s' : Set A) :
        zeroLocus π’œ (s βˆͺ s') = zeroLocus π’œ s ∩ zeroLocus π’œ s'
        source
        theorem ProjectiveSpectrum.vanishingIdeal_union {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (t t' : Set (ProjectiveSpectrum π’œ)) :
        vanishingIdeal (t βˆͺ t') = vanishingIdeal t βŠ“ vanishingIdeal t'
        source
        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) :
        zeroLocus π’œ ↑(⨆ (i : Ξ³), I i) = β‹‚ (i : Ξ³), zeroLocus π’œ ↑(I i)
        source
        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 π’œ) :
        zeroLocus π’œ ↑(⨆ (i : Ξ³), I i) = β‹‚ (i : Ξ³), zeroLocus π’œ ↑(I i)
        source
        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) :
        zeroLocus π’œ (⋃ (i : Ξ³), s i) = β‹‚ (i : Ξ³), zeroLocus π’œ (s i)
        source
        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)) :
        zeroLocus π’œ (⋃ s' ∈ s, s') = β‹‚ s' ∈ s, zeroLocus π’œ s'
        source
        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 π’œ)) :
        vanishingIdeal (⋃ (i : Ξ³), t i) = β¨… (i : Ξ³), vanishingIdeal (t i)
        source
        theorem ProjectiveSpectrum.zeroLocus_inf {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (I J : Ideal A) :
        zeroLocus π’œ ↑(I βŠ“ J) = zeroLocus π’œ ↑I βˆͺ zeroLocus π’œ ↑J
        source
        theorem ProjectiveSpectrum.union_zeroLocus {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (s s' : Set A) :
        zeroLocus π’œ s βˆͺ zeroLocus π’œ s' = zeroLocus π’œ ↑(Ideal.span s βŠ“ Ideal.span s')
        source
        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 J : Ideal A) :
        zeroLocus π’œ ↑(I * J) = zeroLocus π’œ ↑I βˆͺ zeroLocus π’œ ↑J
        source
        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 J : HomogeneousIdeal π’œ) :
        zeroLocus π’œ ↑(I * J) = zeroLocus π’œ ↑I βˆͺ zeroLocus π’œ ↑J
        source
        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 g : A) :
        zeroLocus π’œ {f * g} = zeroLocus π’œ {f} βˆͺ zeroLocus π’œ {g}
        source
        @[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) :
        zeroLocus π’œ {f ^ n} = zeroLocus π’œ {f}
        source
        theorem ProjectiveSpectrum.sup_vanishingIdeal_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (t t' : Set (ProjectiveSpectrum π’œ)) :
        vanishingIdeal t βŠ” vanishingIdeal t' ≀ vanishingIdeal (t ∩ t')
        source
        theorem ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] {f : A} {I : ProjectiveSpectrum π’œ} :
        I ∈ (zeroLocus π’œ {f})ᢜ ↔ f βˆ‰ I.asHomogeneousIdeal
        source
        @[deprecated ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem (since := "2025-05-23")]
        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 ∈ (zeroLocus π’œ {f})ᢜ ↔ f βˆ‰ I.asHomogeneousIdeal

        Alias of ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem.

        source
        instance ProjectiveSpectrum.zariskiTopology {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        TopologicalSpace (ProjectiveSpectrum π’œ)

        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
        source
        def ProjectiveSpectrum.top {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
        TopCat

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

        Equations
        Instances For
          source
          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ᢜ = zeroLocus π’œ s
          source
          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 = zeroLocus π’œ s
          source
          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) :
          IsClosed (zeroLocus π’œ s)
          source
          theorem ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (t : Set (ProjectiveSpectrum π’œ)) :
          zeroLocus π’œ ↑(vanishingIdeal t) = closure t
          source
          theorem ProjectiveSpectrum.vanishingIdeal_closure {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (t : Set (ProjectiveSpectrum π’œ)) :
          vanishingIdeal (closure t) = vanishingIdeal t
          source
          def ProjectiveSpectrum.basicOpen {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (r : A) :
          TopologicalSpace.Opens (ProjectiveSpectrum π’œ)

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

          Equations
          Instances For
            source
            @[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 ∈ basicOpen π’œ f ↔ f βˆ‰ x.asHomogeneousIdeal
            source
            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 ∈ ↑(basicOpen π’œ f) ↔ f βˆ‰ x.asHomogeneousIdeal
            source
            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} :
            IsOpen ↑(basicOpen π’œ a)
            source
            @[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) :
            ↑(basicOpen π’œ r) = (zeroLocus π’œ {r})ᢜ
            source
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
            basicOpen π’œ 1 = ⊀
            source
            @[simp]
            theorem ProjectiveSpectrum.basicOpen_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
            basicOpen π’œ 0 = βŠ₯
            source
            theorem ProjectiveSpectrum.basicOpen_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] (f g : A) :
            basicOpen π’œ (f * g) = basicOpen π’œ f βŠ“ basicOpen π’œ g
            source
            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 g : A) :
            basicOpen π’œ (f * g) ≀ basicOpen π’œ f
            source
            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 g : A) :
            basicOpen π’œ (f * g) ≀ basicOpen π’œ g
            source
            @[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) :
            basicOpen π’œ (f ^ n) = basicOpen π’œ f
            source
            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) :
            basicOpen π’œ f = ⨆ (i : β„•), basicOpen π’œ ((GradedAlgebra.proj π’œ i) f)
            source
            theorem ProjectiveSpectrum.isTopologicalBasis_basic_opens {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
            TopologicalSpace.IsTopologicalBasis (Set.range fun (r : A) => ↑(basicOpen π’œ r))

            The specialization order #

            We endow ProjectiveSpectrum π’œ with a partial order, where x ≀ y if and only if y ∈ closure {x}.

            source
            instance ProjectiveSpectrum.instPartialOrder {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (π’œ : β„• β†’ Submodule R A) [GradedAlgebra π’œ] :
            PartialOrder (ProjectiveSpectrum π’œ)
            Equations
            source
            @[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 y : ProjectiveSpectrum π’œ) :
            x.asHomogeneousIdeal ≀ y.asHomogeneousIdeal ↔ x ≀ y
            source
            @[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 y : ProjectiveSpectrum π’œ) :
            x.asHomogeneousIdeal < y.asHomogeneousIdeal ↔ x < y
            source
            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 y : ProjectiveSpectrum π’œ) :
            x ≀ y ↔ y ∈ closure {x}