mathlib3 documentation

algebraic_geometry.prime_spectrum.basic

Prime spectrum of a commutative ring #

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

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

@[ext]
structure prime_spectrum (R : Type u) [comm_ring R] :

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.

Instances for prime_spectrum
theorem prime_spectrum.ext {R : Type u} {_inst_1 : comm_ring R} (x y : prime_spectrum R) (h : x.as_ideal = y.as_ideal) :
x = y
theorem prime_spectrum.ext_iff {R : Type u} {_inst_1 : comm_ring R} (x y : prime_spectrum R) :
@[protected, instance]

The prime spectrum of the zero ring is empty.

@[simp]

The map from the direct sum of prime spectra to the prime spectrum of a direct product.

Equations

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

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

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

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) :
theorem prime_spectrum.zero_locus_Union {R : Type u} [comm_ring R] {ι : Sort u_1} (s : ι set R) :
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'
@[simp]
@[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
@[protected, instance]

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

Equations
@[simp]
theorem prime_spectrum.comap_comp {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {S' : Type u_1} [comm_ring S'] (f : R →+* S) (g : S →+* S') :
theorem prime_spectrum.comap_comp_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {S' : Type u_1} [comm_ring S'] (f : R →+* S) (g : S →+* S') (x : prime_spectrum S') :

The comap of a surjective ring homomorphism is a closed embedding between the prime spectra.

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

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

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

nhds as an order embedding.

Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations

If x specializes to y, then there is a natural map from the localization of y to the localization of x.

Equations

The closed point in the prime spectrum of a local ring.

Equations