mathlib documentation

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 #

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.

@[protected, instance]

The prime spectrum of the zero ring is empty.

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
@[ext]
theorem prime_spectrum.ext {R : Type u} [comm_ring R] {x y : prime_spectrum R} :
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]
def prime_spectrum.vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum 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 (prime_spectrum R)) :
(prime_spectrum.vanishing_ideal t) = {f : R | ∀ (x : prime_spectrum R), x tf x.as_ideal}
theorem prime_spectrum.mem_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) (f : R) :

zero_locus and vanishing_ideal form a galois connection.

zero_locus and vanishing_ideal form a galois connection.

theorem prime_spectrum.zero_locus_supr {R : Type u} [comm_ring R] {ι : Sort u_1} (I : ι → ideal R) :
prime_spectrum.zero_locus (⨆ (i : ι), I i) = ⋂ (i : ι), prime_spectrum.zero_locus (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 : ι), prime_spectrum.zero_locus (s 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), prime_spectrum.zero_locus s'
theorem prime_spectrum.vanishing_ideal_Union {R : Type u} [comm_ring R] {ι : Sort u_1} (t : ι → set (prime_spectrum R)) :
prime_spectrum.vanishing_ideal (⋃ (i : ι), t i) = ⨅ (i : ι), prime_spectrum.vanishing_ideal (t i)
@[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) :
@[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
theorem prime_spectrum.is_open_iff {R : Type u} [comm_ring R] (U : set (prime_spectrum R)) :
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
@[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) :
@[simp]
@[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') :
theorem prime_spectrum.comap_continuous {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) :

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

Equations
@[simp]
@[simp]
theorem prime_spectrum.basic_open_pow {R : Type u} [comm_ring R] (f : R) (n : ) (hn : 0 < n) :
@[protected, instance]

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

@[simp]
@[simp]
theorem prime_spectrum.as_ideal_lt_as_ideal {R : Type u} [comm_ring R] (x y : prime_spectrum R) :
theorem prime_spectrum.le_iff_mem_closure {R : Type u} [comm_ring R] (x y : prime_spectrum R) :
x y y closure {x}