mathlib documentation

algebraic_geometry.projective_spectrum.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 projective_spectrum.ext_iff {R : Type u_1} {A : Type u_2} {_inst_1 : comm_semiring R} {_inst_2 : comm_ring A} {_inst_3 : algebra R A} {π’œ : β„• β†’ submodule R A} {_inst_4 : graded_algebra π’œ} (x y : projective_spectrum π’œ) :
@[nolint, ext]
structure projective_spectrum {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
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 projective_spectrum
theorem projective_spectrum.ext {R : Type u_1} {A : Type u_2} {_inst_1 : comm_semiring R} {_inst_2 : comm_ring A} {_inst_3 : algebra R A} {π’œ : β„• β†’ submodule R A} {_inst_4 : graded_algebra π’œ} (x y : projective_spectrum π’œ) (h : x.as_homogeneous_ideal = y.as_homogeneous_ideal) :
x = y
def projective_spectrum.zero_locus {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (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, zero_locus s is exactly the subset of projective_spectrum π’œ where all "functions" in s vanish simultaneously.

Equations
@[simp]
@[simp]
def projective_spectrum.vanishing_ideal {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] (t : set (projective_spectrum π’œ)) :

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, vanishing_ideal t is exactly the ideal of A consisting of all "functions" that vanish on all of t.

Equations

zero_locus and vanishing_ideal form a galois connection.

zero_locus and vanishing_ideal form a galois connection.

theorem projective_spectrum.zero_locus_anti_mono {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] {s t : set A} (h : s βŠ† t) :
@[simp]
@[simp]
theorem projective_spectrum.zero_locus_empty_of_one_mem {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] {s : set A} (h : 1 ∈ s) :
@[simp]
@[simp]
theorem projective_spectrum.zero_locus_supr_ideal {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] {Ξ³ : Sort u_3} (I : Ξ³ β†’ ideal A) :
theorem projective_spectrum.zero_locus_supr_homogeneous_ideal {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] {Ξ³ : Sort u_3} (I : Ξ³ β†’ homogeneous_ideal π’œ) :
theorem projective_spectrum.zero_locus_Union {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] {Ξ³ : Sort u_3} (s : Ξ³ β†’ set A) :
projective_spectrum.zero_locus π’œ (⋃ (i : Ξ³), s i) = β‹‚ (i : Ξ³), projective_spectrum.zero_locus π’œ (s i)
theorem projective_spectrum.zero_locus_bUnion {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (s : set (set A)) :
projective_spectrum.zero_locus π’œ (⋃ (s' : set A) (H : s' ∈ s), s') = β‹‚ (s' : set A) (H : s' ∈ s), projective_spectrum.zero_locus π’œ s'
theorem projective_spectrum.vanishing_ideal_Union {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] {Ξ³ : Sort u_3} (t : Ξ³ β†’ set (projective_spectrum π’œ)) :
@[simp]
theorem projective_spectrum.zero_locus_singleton_pow {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (f : A) (n : β„•) (hn : 0 < n) :
@[protected, instance]

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 projective_spectrum.Top {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :

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

Equations
theorem projective_spectrum.is_open_iff {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U : set (projective_spectrum π’œ)) :
theorem projective_spectrum.is_closed_zero_locus {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (s : set A) :
def projective_spectrum.basic_open {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (r : A) :

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

Equations
@[simp]
theorem projective_spectrum.mem_basic_open {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (f : A) (x : projective_spectrum π’œ) :
theorem projective_spectrum.is_open_basic_open {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] {a : A} :
@[simp]
theorem projective_spectrum.basic_open_one {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
@[simp]
theorem projective_spectrum.basic_open_zero {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
@[simp]
theorem projective_spectrum.basic_open_pow {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (f : A) (n : β„•) (hn : 0 < n) :

The specialization order #

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

@[simp]
theorem projective_spectrum.le_iff_mem_closure {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (x y : projective_spectrum π’œ) :