# mathlib3documentation

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 #

• R is a commutative semiring;
• A is a commutative ring and an R-algebra;
• 𝒜 : ℕ → submodule R A is the grading of A;

## Main definitions #

• projective_spectrum 𝒜: 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.
• projective_spectrum.zero_locus 𝒜 s: The zero locus of a subset s of A is the subset of projective_spectrum 𝒜 consisting of all relevant homogeneous prime ideals that contain s.
• projective_spectrum.vanishing_ideal t: The vanishing ideal of a subset t of projective_spectrum 𝒜 is the intersection of points in t (viewed as relevant homogeneous prime ideals).
• projective_spectrum.Top: the topological space of projective_spectrum 𝒜 endowed with the Zariski topology.
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 : A} {𝒜 : A} {_inst_4 : graded_algebra 𝒜} (x y : projective_spectrum 𝒜) :
@[nolint, ext]
structure projective_spectrum {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
Type u_2
• as_homogeneous_ideal :
• is_prime :
• not_irrelevant_le :

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 : A} {𝒜 : A} {_inst_4 : graded_algebra 𝒜} (x y : projective_spectrum 𝒜)  :
x = y
def projective_spectrum.zero_locus {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (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]
theorem projective_spectrum.mem_zero_locus {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (x : projective_spectrum 𝒜) (s : set A) :
@[simp]
theorem projective_spectrum.zero_locus_span {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (s : set A) :
def projective_spectrum.vanishing_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] {𝒜 : A} (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, vanishing_ideal t is exactly the ideal of A consisting of all "functions" that vanish on all of t.

Equations
theorem projective_spectrum.coe_vanishing_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] {𝒜 : A} (t : set ) :
= {f : A | (x : , x t
theorem projective_spectrum.mem_vanishing_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] {𝒜 : A} (t : set ) (f : A) :
(x : , x t
@[simp]
theorem projective_spectrum.vanishing_ideal_singleton {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] {𝒜 : A} (x : projective_spectrum 𝒜) :
theorem projective_spectrum.subset_zero_locus_iff_le_vanishing_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] {𝒜 : A} (t : set ) (I : ideal A) :
theorem projective_spectrum.gc_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
galois_connection (λ (I : ideal A), (λ (t : (set ᵒᵈ),

zero_locus and vanishing_ideal form a galois connection.

theorem projective_spectrum.gc_set {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
galois_connection (λ (s : set A), (λ (t : (set ᵒᵈ),

zero_locus and vanishing_ideal form a galois connection.

theorem projective_spectrum.gc_homogeneous_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
galois_connection (λ (I : , (λ (t : (set ᵒᵈ),
theorem projective_spectrum.subset_zero_locus_iff_subset_vanishing_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (t : set ) (s : set A) :
theorem projective_spectrum.subset_vanishing_ideal_zero_locus {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (s : set A) :
theorem projective_spectrum.ideal_le_vanishing_ideal_zero_locus {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (I : ideal A) :
theorem projective_spectrum.subset_zero_locus_vanishing_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (t : set ) :
theorem projective_spectrum.zero_locus_anti_mono {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {s t : set A} (h : s t) :
theorem projective_spectrum.zero_locus_anti_mono_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {s t : ideal A} (h : s t) :
theorem projective_spectrum.zero_locus_anti_mono_homogeneous_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {s t : homogeneous_ideal 𝒜} (h : s t) :
theorem projective_spectrum.vanishing_ideal_anti_mono {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {s t : set } (h : s t) :
theorem projective_spectrum.zero_locus_bot {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
@[simp]
theorem projective_spectrum.zero_locus_singleton_zero {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
@[simp]
theorem projective_spectrum.zero_locus_empty {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
@[simp]
theorem projective_spectrum.vanishing_ideal_univ {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
theorem projective_spectrum.zero_locus_empty_of_one_mem {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {s : set A} (h : 1 s) :
@[simp]
theorem projective_spectrum.zero_locus_singleton_one {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
@[simp]
theorem projective_spectrum.zero_locus_univ {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
theorem projective_spectrum.zero_locus_sup_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (I J : ideal A) :
theorem projective_spectrum.zero_locus_sup_homogeneous_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (I J : homogeneous_ideal 𝒜) :
theorem projective_spectrum.zero_locus_union {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (s s' : set A) :
theorem projective_spectrum.vanishing_ideal_union {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (t t' : set ) :
theorem projective_spectrum.zero_locus_supr_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {γ : Sort u_3} (I : γ ) :
( (i : γ), I i) = (i : γ),
theorem projective_spectrum.zero_locus_supr_homogeneous_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {γ : Sort u_3} (I : γ ) :
( (i : γ), I i) = (i : γ),
theorem projective_spectrum.zero_locus_Union {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {γ : Sort u_3} (s : γ set A) :
( (i : γ), s i) = (i : γ),
theorem projective_spectrum.zero_locus_bUnion {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (s : set (set A)) :
( (s' : set A) (H : s' s), s') = (s' : set A) (H : s' s),
theorem projective_spectrum.vanishing_ideal_Union {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {γ : Sort u_3} (t : γ ) :
theorem projective_spectrum.zero_locus_inf {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (I J : ideal A) :
theorem projective_spectrum.union_zero_locus {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (s s' : set A) :
theorem projective_spectrum.zero_locus_mul_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (I J : ideal A) :
theorem projective_spectrum.zero_locus_mul_homogeneous_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (I J : homogeneous_ideal 𝒜) :
theorem projective_spectrum.zero_locus_singleton_mul {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f g : A) :
@[simp]
theorem projective_spectrum.zero_locus_singleton_pow {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f : A) (n : ) (hn : 0 < n) :
theorem projective_spectrum.sup_vanishing_ideal_le {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (t t' : set ) :
theorem projective_spectrum.mem_compl_zero_locus_iff_not_mem {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {f : A} {I : projective_spectrum 𝒜} :
@[protected, instance]
def projective_spectrum.zariski_topology {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :

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_ring A] [ A] (𝒜 : A)  :

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_ring A] [ A] (𝒜 : A) (U : set ) :
(s : set A),
theorem projective_spectrum.is_closed_iff_zero_locus {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (Z : set ) :
(s : set A),
theorem projective_spectrum.is_closed_zero_locus {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (s : set A) :
theorem projective_spectrum.zero_locus_vanishing_ideal_eq_closure {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (t : set ) :
theorem projective_spectrum.vanishing_ideal_closure {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (t : set ) :
def projective_spectrum.basic_open {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (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_ring A] [ A] (𝒜 : A) (f : A) (x : projective_spectrum 𝒜) :
theorem projective_spectrum.mem_coe_basic_open {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f : A) (x : projective_spectrum 𝒜) :
theorem projective_spectrum.is_open_basic_open {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) {a : A} :
@[simp]
theorem projective_spectrum.basic_open_eq_zero_locus_compl {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (r : A) :
@[simp]
theorem projective_spectrum.basic_open_one {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
@[simp]
theorem projective_spectrum.basic_open_zero {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
theorem projective_spectrum.basic_open_mul {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f g : A) :
theorem projective_spectrum.basic_open_mul_le_left {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f g : A) :
theorem projective_spectrum.basic_open_mul_le_right {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f g : A) :
@[simp]
theorem projective_spectrum.basic_open_pow {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f : A) (n : ) (hn : 0 < n) :
theorem projective_spectrum.basic_open_eq_union_of_projection {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (f : A) :
= (i : ),

## The specialization order #

We endow projective_spectrum 𝒜 with a partial order, where x ≤ y if and only if y ∈ closure {x}.

@[protected, instance]
def projective_spectrum.partial_order {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A)  :
Equations
@[simp]
theorem projective_spectrum.as_ideal_le_as_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (x y : projective_spectrum 𝒜) :
@[simp]
theorem projective_spectrum.as_ideal_lt_as_ideal {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (x y : projective_spectrum 𝒜) :
theorem projective_spectrum.le_iff_mem_closure {R : Type u_1} {A : Type u_2} [comm_ring A] [ A] (𝒜 : A) (x y : projective_spectrum 𝒜) :
x y y closure {x}