# mathlibdocumentation

algebraic_geometry.prime_spectrum

# Prime spectrum of a commutative ring #

The prime spectrum of a commutative ring is the type of all prime ideals. It is naturally endowed with a topology: the Zariski topology.

(It is also naturally endowed with a sheaf of rings, which is constructed in algebraic_geometry.structure_sheaf.)

## Main definitions #

• prime_spectrum R: The prime spectrum of a commutative ring R, i.e., the set of all prime ideals of R.
• zero_locus s: The zero locus of a subset s of R is the subset of prime_spectrum R consisting of all prime ideals that contain s.
• vanishing_ideal t: The vanishing ideal of a subset t of prime_spectrum R is the intersection of points in t (viewed as prime ideals).

## Conventions #

We denote subsets of rings with s, s', etc... whereas we denote subsets of prime spectra with t, t', etc...

## Inspiration/contributors #

The contents of this file draw inspiration from https://github.com/ramonfmir/lean-scheme which has contributions from Ramon Fernandez Mir, Kevin Buzzard, Kenny Lau, and Chris Hughes (on an earlier repository).

@[nolint]
def prime_spectrum (R : Type u) [comm_ring R] :
Type u

The prime spectrum of a commutative ring R is the type of all prime ideals of R.

It is naturally endowed with a topology (the Zariski topology), and a sheaf of commutative rings (see algebraic_geometry.structure_sheaf). It is a fundamental building block in algebraic geometry.

Equations
def prime_spectrum.as_ideal {R : Type u} [comm_ring R] (x : prime_spectrum R) :

A method to view a point in the prime spectrum of a commutative ring as an ideal of that ring.

@[instance]
def prime_spectrum.is_prime {R : Type u} [comm_ring R] (x : prime_spectrum R) :

The prime spectrum of the zero ring is empty.

def prime_spectrum.prime_spectrum_prod (R : Type u) [comm_ring R] (S : Type v) [comm_ring S] :

The prime spectrum of R × S is in bijection with the disjoint unions of the prime spectrum of R and the prime spectrum of S.

Equations
@[simp]
@[simp]
@[ext]
theorem prime_spectrum.ext {R : Type u} [comm_ring R] {x y : prime_spectrum R} :
x = y
def prime_spectrum.zero_locus {R : Type u} [comm_ring R] (s : set R) :

The zero locus of a set s of elements of a commutative ring R is the set of all prime ideals of the ring that contain the set s.

An element f of R can be thought of as a dependent function on the prime spectrum of R. At a point x (a prime ideal) the function (i.e., element) f takes values in the quotient ring R modulo the prime ideal x. In this manner, zero_locus s is exactly the subset of prime_spectrum R where all "functions" in s vanish simultaneously.

Equations
@[simp]
theorem prime_spectrum.mem_zero_locus {R : Type u} [comm_ring R] (x : prime_spectrum R) (s : set R) :
@[simp]
theorem prime_spectrum.zero_locus_span {R : Type u} [comm_ring R] (s : set R) :
def prime_spectrum.vanishing_ideal {R : Type u} [comm_ring R] (t : set ) :

The vanishing ideal of a set t of points of the prime spectrum of a commutative ring R is the intersection of all the prime ideals in the set t.

An element f of R can be thought of as a dependent function on the prime spectrum of R. At a point x (a prime ideal) the function (i.e., element) f takes values in the quotient ring R modulo the prime ideal x. In this manner, vanishing_ideal t is exactly the ideal of R consisting of all "functions" that vanish on all of t.

Equations
theorem prime_spectrum.coe_vanishing_ideal {R : Type u} [comm_ring R] (t : set ) :
= {f : R | ∀ (x : , x tf x.as_ideal}
theorem prime_spectrum.mem_vanishing_ideal {R : Type u} [comm_ring R] (t : set ) (f : R) :
∀ (x : , x tf x.as_ideal
@[simp]
theorem prime_spectrum.gc (R : Type u) [comm_ring R] :
galois_connection (λ (I : ideal R), (λ (t : order_dual (set (prime_spectrum R))),

zero_locus and vanishing_ideal form a galois connection.

theorem prime_spectrum.gc_set (R : Type u) [comm_ring R] :
galois_connection (λ (s : set R), (λ (t : order_dual (set (prime_spectrum R))),

zero_locus and vanishing_ideal form a galois connection.

@[simp]
@[simp]
theorem prime_spectrum.zero_locus_radical {R : Type u} [comm_ring R] (I : ideal R) :
theorem prime_spectrum.zero_locus_anti_mono {R : Type u} [comm_ring R] {s t : set R} (h : s t) :
theorem prime_spectrum.zero_locus_anti_mono_ideal {R : Type u} [comm_ring R] {s t : ideal R} (h : s t) :
theorem prime_spectrum.vanishing_ideal_anti_mono {R : Type u} [comm_ring R] {s t : set } (h : s t) :
theorem prime_spectrum.zero_locus_bot {R : Type u} [comm_ring R] :
@[simp]
@[simp]
theorem prime_spectrum.zero_locus_empty {R : Type u} [comm_ring R] :
@[simp]
theorem prime_spectrum.vanishing_ideal_univ {R : Type u} [comm_ring R] :
theorem prime_spectrum.zero_locus_empty_of_one_mem {R : Type u} [comm_ring R] {s : set R} (h : 1 s) :
@[simp]
@[simp]
theorem prime_spectrum.zero_locus_univ {R : Type u} [comm_ring R] :
theorem prime_spectrum.zero_locus_sup {R : Type u} [comm_ring R] (I J : ideal R) :
theorem prime_spectrum.zero_locus_union {R : Type u} [comm_ring R] (s s' : set R) :
theorem prime_spectrum.vanishing_ideal_union {R : Type u} [comm_ring R] (t t' : set ) :
theorem prime_spectrum.zero_locus_supr {R : Type u} [comm_ring R] {ι : Sort u_1} (I : ι → ) :
prime_spectrum.zero_locus (⨆ (i : ι), I i) = ⋂ (i : ι),
theorem prime_spectrum.zero_locus_Union {R : Type u} [comm_ring R] {ι : Sort u_1} (s : ι → set R) :
prime_spectrum.zero_locus (⋃ (i : ι), s i) = ⋂ (i : ι),
theorem prime_spectrum.zero_locus_bUnion {R : Type u} [comm_ring R] (s : set (set R)) :
prime_spectrum.zero_locus (⋃ (s' : set R) (H : s' s), s') = ⋂ (s' : set R) (H : s' s),
theorem prime_spectrum.vanishing_ideal_Union {R : Type u} [comm_ring R] {ι : Sort u_1} (t : ι → ) :
prime_spectrum.vanishing_ideal (⋃ (i : ι), t i) = ⨅ (i : ι),
theorem prime_spectrum.zero_locus_inf {R : Type u} [comm_ring R] (I J : ideal R) :
theorem prime_spectrum.union_zero_locus {R : Type u} [comm_ring R] (s s' : set R) :
theorem prime_spectrum.zero_locus_mul {R : Type u} [comm_ring R] (I J : ideal R) :
theorem prime_spectrum.zero_locus_singleton_mul {R : Type u} [comm_ring R] (f g : R) :
@[simp]
theorem prime_spectrum.zero_locus_pow {R : Type u} [comm_ring R] (I : ideal R) {n : } (hn : 0 < n) :
@[simp]
theorem prime_spectrum.zero_locus_singleton_pow {R : Type u} [comm_ring R] (f : R) (n : ) (hn : 0 < n) :
theorem prime_spectrum.sup_vanishing_ideal_le {R : Type u} [comm_ring R] (t t' : set ) :
@[instance]
def prime_spectrum.zariski_topology {R : Type u} [comm_ring R] :

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
theorem prime_spectrum.is_open_iff {R : Type u} [comm_ring R] (U : set ) :
∃ (s : set R),
theorem prime_spectrum.is_closed_iff_zero_locus {R : Type u} [comm_ring R] (Z : set ) :
∃ (s : set R),
theorem prime_spectrum.is_closed_zero_locus {R : Type u} [comm_ring R] (s : set R) :
theorem prime_spectrum.vanishing_ideal_closure {R : Type u} [comm_ring R] (t : set ) :
def prime_spectrum.comap {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) :

The function between prime spectra of commutative rings induced by a ring homomorphism. This function is continuous.

Equations
• = λ (y : , , _⟩
@[simp]
theorem prime_spectrum.comap_as_ideal {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (y : prime_spectrum S) :
y).as_ideal =
@[simp]
theorem prime_spectrum.comap_id {R : Type u} [comm_ring R] :
@[simp]
theorem prime_spectrum.comap_comp {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {S' : Type u_1} [comm_ring S'] (f : R →+* S) (g : S →+* S') :
@[simp]
theorem prime_spectrum.preimage_comap_zero_locus {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (s : set R) :
theorem prime_spectrum.comap_continuous {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) :
def prime_spectrum.basic_open {R : Type u} [comm_ring R] (r : R) :

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

Equations
@[simp]
theorem prime_spectrum.mem_basic_open {R : Type u} [comm_ring R] (f : R) (x : prime_spectrum R) :
theorem prime_spectrum.is_open_basic_open {R : Type u} [comm_ring R] {a : R} :
@[simp]
theorem prime_spectrum.basic_open_eq_zero_locus_compl {R : Type u} [comm_ring R] (r : R) :
@[simp]
theorem prime_spectrum.basic_open_one {R : Type u} [comm_ring R] :
@[simp]
theorem prime_spectrum.basic_open_zero {R : Type u} [comm_ring R] :
theorem prime_spectrum.basic_open_le_basic_open_iff {R : Type u} [comm_ring R] (f g : R) :
theorem prime_spectrum.basic_open_mul {R : Type u} [comm_ring R] (f g : R) :
theorem prime_spectrum.basic_open_mul_le_left {R : Type u} [comm_ring R] (f g : R) :
theorem prime_spectrum.basic_open_mul_le_right {R : Type u} [comm_ring R] (f g : R) :
@[simp]
theorem prime_spectrum.basic_open_pow {R : Type u} [comm_ring R] (f : R) (n : ) (hn : 0 < n) :
theorem prime_spectrum.is_compact_basic_open {R : Type u} [comm_ring R] (f : R) :
@[instance]
def prime_spectrum.compact_space {R : Type u} [comm_ring R] :

The prime spectrum of a commutative ring is a compact topological space.

## The specialization order #

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

TODO: maybe define sober topological spaces, and generalise this instance to those

@[instance]
def prime_spectrum.partial_order {R : Type u} [comm_ring R] :
Equations
@[simp]
theorem prime_spectrum.as_ideal_le_as_ideal {R : Type u} [comm_ring R] (x y : prime_spectrum R) :
x y
@[simp]
theorem prime_spectrum.as_ideal_lt_as_ideal {R : Type u} [comm_ring R] (x y : prime_spectrum R) :
x < y
theorem prime_spectrum.le_iff_mem_closure {R : Type u} [comm_ring R] (x y : prime_spectrum R) :
x y y closure {x}