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 #

• R is a commutative semiring;
• A is a commutative ring and an R-algebra;
• ๐ : โ โ Submodule R A is the grading of A;

Main definitions #

• ProjectiveSpectrum ๐: The projective spectrum of a graded ring A, or equivalently, the set of all homogeneous ideals of A that is both prime and relevant i.e. not containing irrelevant ideal. Henceforth, we call elements of projective spectrum relevant homogeneous prime ideals.
• ProjectiveSpectrum.zeroLocus ๐ s: The zero locus of a subset s of A is the subset of ProjectiveSpectrum ๐ consisting of all relevant homogeneous prime ideals that contain s.
• ProjectiveSpectrum.vanishingIdeal t: The vanishing ideal of a subset t of ProjectiveSpectrum ๐ is the intersection of points in t (viewed as relevant homogeneous prime ideals).
• ProjectiveSpectrum.Top: the topological space of ProjectiveSpectrum ๐ endowed with the Zariski topology.
theorem ProjectiveSpectrum.ext {R : Type u_1} {A : Type u_2} :
โ {inst : } {inst_1 : } {inst_2 : Algebra R A} {๐ : โ โ } {inst_3 : GradedAlgebra ๐} (x y : ), x.asHomogeneousIdeal = y.asHomogeneousIdeal โ x = y
theorem ProjectiveSpectrum.ext_iff {R : Type u_1} {A : Type u_2} :
โ {inst : } {inst_1 : } {inst_2 : Algebra R A} {๐ : โ โ } {inst_3 : GradedAlgebra ๐} (x y : ), x = y โ x.asHomogeneousIdeal = y.asHomogeneousIdeal
structure ProjectiveSpectrum {R : Type u_1} {A : Type u_2} [] [] [Algebra 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.

• asHomogeneousIdeal : HomogeneousIdeal ๐
• isPrime : self.asHomogeneousIdeal.toIdeal.IsPrime
• not_irrelevant_le : ยฌ โค self.asHomogeneousIdeal
Instances For
theorem ProjectiveSpectrum.isPrime {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (self : ) :
self.asHomogeneousIdeal.toIdeal.IsPrime
theorem ProjectiveSpectrum.not_irrelevant_le {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (self : ) :
ยฌ โค self.asHomogeneousIdeal
def ProjectiveSpectrum.zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (s : Set A) :
Set ()

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
• = {x : | s โ โx.asHomogeneousIdeal}
Instances For
@[simp]
theorem ProjectiveSpectrum.mem_zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : ) (s : Set A) :
x โ โ s โ โx.asHomogeneousIdeal
@[simp]
theorem ProjectiveSpectrum.zeroLocus_span {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (s : Set A) :
ProjectiveSpectrum.zeroLocus ๐ โ() =
def ProjectiveSpectrum.vanishingIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (t : Set ()) :

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
• = โจ x โ t, x.asHomogeneousIdeal
Instances For
theorem ProjectiveSpectrum.coe_vanishingIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (t : Set ()) :
= {f : A | โ x โ t, f โ x.asHomogeneousIdeal}
theorem ProjectiveSpectrum.mem_vanishingIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (t : Set ()) (f : A) :
โ โ x โ t, f โ x.asHomogeneousIdeal
@[simp]
theorem ProjectiveSpectrum.vanishingIdeal_singleton {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (x : ) :
= x.asHomogeneousIdeal
theorem ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (t : Set ()) (I : ) :
t โ ProjectiveSpectrum.zeroLocus ๐ โI โ I โค .toIdeal
theorem ProjectiveSpectrum.gc_ideal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
GaloisConnection (fun (I : ) => ProjectiveSpectrum.zeroLocus ๐ โI) fun (t : (Set ())แตแต) => .toIdeal

zeroLocus and vanishingIdeal form a galois connection.

theorem ProjectiveSpectrum.gc_set {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
GaloisConnection (fun (s : Set A) => ) fun (t : (Set ())แตแต) =>

zeroLocus and vanishingIdeal form a galois connection.

theorem ProjectiveSpectrum.gc_homogeneousIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
GaloisConnection (fun (I : HomogeneousIdeal ๐) => ProjectiveSpectrum.zeroLocus ๐ โI) fun (t : (Set ())แตแต) =>
theorem ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (t : Set ()) (s : Set A) :
theorem ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (s : Set A) :
theorem ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (I : ) :
I โค .toIdeal
theorem ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (I : HomogeneousIdeal ๐) :
theorem ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (t : Set ()) :
theorem ProjectiveSpectrum.zeroLocus_anti_mono {R : Type u_1} {A : Type u_2} [] [] [Algebra 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} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {s : } {t : } (h : s โค t) :
theorem ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {s : HomogeneousIdeal ๐} {t : HomogeneousIdeal ๐} (h : s โค t) :
theorem ProjectiveSpectrum.vanishingIdeal_anti_mono {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {s : Set ()} {t : Set ()} (h : s โ t) :
theorem ProjectiveSpectrum.zeroLocus_bot {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
= Set.univ
@[simp]
theorem ProjectiveSpectrum.zeroLocus_singleton_zero {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
ProjectiveSpectrum.zeroLocus ๐ {0} = Set.univ
@[simp]
theorem ProjectiveSpectrum.zeroLocus_empty {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
= Set.univ
@[simp]
theorem ProjectiveSpectrum.vanishingIdeal_univ {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
theorem ProjectiveSpectrum.zeroLocus_empty_of_one_mem {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {s : Set A} (h : 1 โ s) :
@[simp]
theorem ProjectiveSpectrum.zeroLocus_singleton_one {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
@[simp]
theorem ProjectiveSpectrum.zeroLocus_univ {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
theorem ProjectiveSpectrum.zeroLocus_sup_ideal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (I : ) (J : ) :
theorem ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (I : HomogeneousIdeal ๐) (J : HomogeneousIdeal ๐) :
theorem ProjectiveSpectrum.zeroLocus_union {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (s : Set A) (s' : Set A) :
theorem ProjectiveSpectrum.vanishingIdeal_union {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (t : Set ()) (t' : Set ()) :
theorem ProjectiveSpectrum.zeroLocus_iSup_ideal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {ฮณ : Sort u_3} (I : ฮณ โ ) :
ProjectiveSpectrum.zeroLocus ๐ โ(โจ (i : ฮณ), I i) = โ (i : ฮณ), ProjectiveSpectrum.zeroLocus ๐ โ(I i)
theorem ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra 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} [] [] [Algebra 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} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (s : Set (Set A)) :
ProjectiveSpectrum.zeroLocus ๐ (โ s' โ s, s') = โ s' โ s,
theorem ProjectiveSpectrum.vanishingIdeal_iUnion {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {ฮณ : Sort u_3} (t : ฮณ โ Set ()) :
ProjectiveSpectrum.vanishingIdeal (โ (i : ฮณ), t i) = โจ (i : ฮณ),
theorem ProjectiveSpectrum.zeroLocus_inf {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (I : ) (J : ) :
theorem ProjectiveSpectrum.union_zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (s : Set A) (s' : Set A) :
theorem ProjectiveSpectrum.zeroLocus_mul_ideal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (I : ) (J : ) :
ProjectiveSpectrum.zeroLocus ๐ โ(I * J) = ProjectiveSpectrum.zeroLocus ๐ โI โช ProjectiveSpectrum.zeroLocus ๐ โJ
theorem ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal {R : Type u_1} {A : Type u_2} [] [] [Algebra 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} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (g : A) :
@[simp]
theorem ProjectiveSpectrum.zeroLocus_singleton_pow {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (n : โ) (hn : 0 < n) :
theorem ProjectiveSpectrum.sup_vanishingIdeal_le {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (t : Set ()) (t' : Set ()) :
theorem ProjectiveSpectrum.mem_compl_zeroLocus_iff_not_mem {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {f : A} {I : } :
I โ (ProjectiveSpectrum.zeroLocus ๐ {f})แถ โ f โ I.asHomogeneousIdeal
instance ProjectiveSpectrum.zariskiTopology {R : Type u_1} {A : Type u_2} [] [] [Algebra 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} [] [] [Algebra 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} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : Set ()) :
โ โ (s : Set A), Uแถ =
theorem ProjectiveSpectrum.isClosed_iff_zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (Z : Set ()) :
โ โ (s : Set A), Z =
theorem ProjectiveSpectrum.isClosed_zeroLocus {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (s : Set A) :
theorem ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (t : Set ()) :
theorem ProjectiveSpectrum.vanishingIdeal_closure {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (t : Set ()) :
def ProjectiveSpectrum.basicOpen {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (r : A) :

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

Equations
• = { carrier := {x : | r โ x.asHomogeneousIdeal}, is_open' := โฏ }
Instances For
@[simp]
theorem ProjectiveSpectrum.mem_basicOpen {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (x : ) :
x โ โ f โ x.asHomogeneousIdeal
theorem ProjectiveSpectrum.mem_coe_basicOpen {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (x : ) :
x โ โ() โ f โ x.asHomogeneousIdeal
theorem ProjectiveSpectrum.isOpen_basicOpen {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {a : A} :
IsOpen โ()
@[simp]
theorem ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (r : A) :
โ() = (ProjectiveSpectrum.zeroLocus ๐ {r})แถ
@[simp]
theorem ProjectiveSpectrum.basicOpen_one {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
@[simp]
theorem ProjectiveSpectrum.basicOpen_zero {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
theorem ProjectiveSpectrum.basicOpen_mul {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (g : A) :
theorem ProjectiveSpectrum.basicOpen_mul_le_left {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (g : A) :
theorem ProjectiveSpectrum.basicOpen_mul_le_right {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (g : A) :
@[simp]
theorem ProjectiveSpectrum.basicOpen_pow {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) (n : โ) (hn : 0 < n) :
theorem ProjectiveSpectrum.basicOpen_eq_union_of_projection {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (f : A) :
= โจ (i : โ), ProjectiveSpectrum.basicOpen ๐ ((GradedAlgebra.proj ๐ i) f)
theorem ProjectiveSpectrum.isTopologicalBasis_basic_opens {R : Type u_1} {A : Type u_2} [] [] [Algebra 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} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
Equations
@[simp]
theorem ProjectiveSpectrum.as_ideal_le_as_ideal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : ) (y : ) :
x.asHomogeneousIdeal โค y.asHomogeneousIdeal โ x โค y
@[simp]
theorem ProjectiveSpectrum.as_ideal_lt_as_ideal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : ) (y : ) :
x.asHomogeneousIdeal < y.asHomogeneousIdeal โ x < y
theorem ProjectiveSpectrum.le_iff_mem_closure {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : ) (y : ) :