# 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] :

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) :

theorem prime_spectrum.punit  :

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] :
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] :

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

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.

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} :
1 s

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

def prime_spectrum.comap {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] :
(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) :

@[instance]
def prime_spectrum.compact_space {R : Type u} [comm_ring R] :

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

def prime_spectrum.basic_open {R : Type u} [comm_ring R] :

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

Equations