mathlib3 documentation

algebraic_geometry.projective_spectrum.topology

Projective spectrum of a graded ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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_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) :
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) :
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'
@[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

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

Equations
@[simp]
@[simp]
@[simp]
@[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}.

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 𝒜) :
x y y closure {x}