# mathlib3documentation

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 #

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

@[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) :
x = y
@[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
noncomputable def prime_spectrum.prime_spectrum_prod (R : Type u) (S : Type v) [comm_ring R] [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
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 t f x.as_ideal}
theorem prime_spectrum.mem_vanishing_ideal {R : Type u} [comm_ring R] (t : set ) (f : R) :
(x : , x t f x.as_ideal
theorem prime_spectrum.gc (R : Type u) [comm_ring R] :
galois_connection (λ (I : ideal R), (λ (t : (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 : (set (prime_spectrum R))ᵒᵈ),

zero_locus and vanishing_ideal form a galois connection.

@[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) :
@[simp]
@[simp]
theorem prime_spectrum.zero_locus_empty_of_one_mem {R : Type u} [comm_ring R] {s : set R} (h : 1 s) :
@[simp]
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) :
@[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 ) :
(s : set R),

The antitone order embedding of closed subsets of Spec R into ideals of R.

Equations
@[protected, instance]
@[protected, instance]
theorem prime_spectrum.preimage_comap_zero_locus_aux {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set R) :
(λ (y : , {as_ideal := , is_prime := _}) ⁻¹' =
def prime_spectrum.comap {R : Type u} {S : Type v} [comm_ring R] [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} {S : Type v} [comm_ring R] [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} {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') :
@[simp]
theorem prime_spectrum.preimage_comap_zero_locus {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set R) :
theorem prime_spectrum.localization_comap_inducing {R : Type u} (S : Type v) [comm_ring R] [comm_ring S] [ S] (M : submonoid R) [ S] :
theorem prime_spectrum.localization_comap_injective {R : Type u} (S : Type v) [comm_ring R] [comm_ring S] [ S] (M : submonoid R) [ S] :
theorem prime_spectrum.localization_comap_embedding {R : Type u} (S : Type v) [comm_ring R] [comm_ring S] [ S] (M : submonoid R) [ S] :
theorem prime_spectrum.localization_comap_range {R : Type u} (S : Type v) [comm_ring R] [comm_ring S] [ S] (M : submonoid R) [ S] :
= {p : | (p.as_ideal)}

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

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]
@[simp]
@[simp]
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) :
@[simp]
theorem prime_spectrum.basic_open_eq_bot_iff {R : Type u} [comm_ring R] (f : R) :
theorem prime_spectrum.localization_away_comap_range {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [ S] (r : R) [ S] :
theorem prime_spectrum.localization_away_open_embedding {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [ S] (r : R) [ S] :
@[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}.

@[protected, instance]
Equations
@[simp]
@[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_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]
def prime_spectrum.unique {R : Type u_1} [field R] :
Equations
noncomputable def prime_spectrum.localization_map_of_specializes {R : Type u} [comm_ring R] {x y : prime_spectrum R} (h : x y) :

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
@[simp]
theorem local_ring.comap_closed_point {R : Type u} [comm_ring R] [local_ring R] {S : Type v} [comm_ring S] [local_ring S] (f : R →+* S)  :
@[simp]