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

Main definitions #

PrimeSpectrum R: The prime spectrum of a commutative ring R, i.e., the set of all prime ideals of R.
zeroLocus s: The zero locus of a subset s of R is the subset of PrimeSpectrum R consisting of all prime ideals that contain s.
vanishingIdeal t: The vanishing ideal of a subset t of PrimeSpectrum 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).

source

theorem PrimeSpectrum.ext_iff {R : Type u} :

∀ {inst : CommRing R} (x y : PrimeSpectrum R), x = y ↔ x.asIdeal = y.asIdeal

source

theorem PrimeSpectrum.ext {R : Type u} :

∀ {inst : CommRing R} (x y : PrimeSpectrum R), x.asIdeal = y.asIdeal → x = y

source

structure PrimeSpectrum (R : Type u) [CommRing R] :

Type u

asIdeal : Ideal R
IsPrime : Ideal.IsPrime s.asIdeal

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 AlgebraicGeometry.StructureSheaf). It is a fundamental building block in algebraic geometry.

Instances For

source

instance PrimeSpectrum.instNonemptyPrimeSpectrum {R : Type u} [CommRing R] [Nontrivial R] :

Nonempty (PrimeSpectrum R)

source

theorem PrimeSpectrum.punit (x : PrimeSpectrum PUnit.{u_1 + 1} ) :

False

The prime spectrum of the zero ring is empty.

source

def PrimeSpectrum.primeSpectrumProdOfSum (R : Type u) (S : Type v) [CommRing R] [CommRing S] :

PrimeSpectrum R ⊕ PrimeSpectrum S → PrimeSpectrum (R × S)

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

Instances For

source

noncomputable def PrimeSpectrum.primeSpectrumProd (R : Type u) (S : Type v) [CommRing R] [CommRing S] :

PrimeSpectrum (R × S) ≃ PrimeSpectrum R ⊕ PrimeSpectrum 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.

Instances For

source

@[simp]

theorem PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal {R : Type u} {S : Type v} [CommRing R] [CommRing S] (x : PrimeSpectrum R) :

(↑(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = Ideal.prod x.asIdeal ⊤

source

@[simp]

theorem PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal {R : Type u} {S : Type v} [CommRing R] [CommRing S] (x : PrimeSpectrum S) :

(↑(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = Ideal.prod ⊤ x.asIdeal

source

def PrimeSpectrum.zeroLocus {R : Type u} [CommRing R] (s : Set R) :

Set (PrimeSpectrum 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, zeroLocus s is exactly the subset of PrimeSpectrum R where all "functions" in s vanish simultaneously.

Instances For

source

@[simp]

theorem PrimeSpectrum.mem_zeroLocus {R : Type u} [CommRing R] (x : PrimeSpectrum R) (s : Set R) :

x ∈ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑x.asIdeal

source

@[simp]

theorem PrimeSpectrum.zeroLocus_span {R : Type u} [CommRing R] (s : Set R) :

PrimeSpectrum.zeroLocus ↑(Ideal.span s) = PrimeSpectrum.zeroLocus s

source

def PrimeSpectrum.vanishingIdeal {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) :

Ideal 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, vanishingIdeal t is exactly the ideal of R consisting of all "functions" that vanish on all of t.

Instances For

source

theorem PrimeSpectrum.coe_vanishingIdeal {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) :

↑(PrimeSpectrum.vanishingIdeal t) = {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}

source

theorem PrimeSpectrum.mem_vanishingIdeal {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) (f : R) :

f ∈ PrimeSpectrum.vanishingIdeal t ↔ ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal

source

@[simp]

theorem PrimeSpectrum.vanishingIdeal_singleton {R : Type u} [CommRing R] (x : PrimeSpectrum R) :

PrimeSpectrum.vanishingIdeal {x} = x.asIdeal

source

theorem PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) (I : Ideal R) :

t ⊆ PrimeSpectrum.zeroLocus ↑I ↔ I ≤ PrimeSpectrum.vanishingIdeal t

source

theorem PrimeSpectrum.gc (R : Type u) [CommRing R] :

GaloisConnection (fun I => PrimeSpectrum.zeroLocus ↑I) fun t => PrimeSpectrum.vanishingIdeal t

zeroLocus and vanishingIdeal form a galois connection.

source

theorem PrimeSpectrum.gc_set (R : Type u) [CommRing R] :

GaloisConnection (fun s => PrimeSpectrum.zeroLocus s) fun t => ↑(PrimeSpectrum.vanishingIdeal t)

zeroLocus and vanishingIdeal form a galois connection.

source

theorem PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal (R : Type u) [CommRing R] (t : Set (PrimeSpectrum R)) (s : Set R) :

t ⊆ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑(PrimeSpectrum.vanishingIdeal t)

source

theorem PrimeSpectrum.subset_vanishingIdeal_zeroLocus {R : Type u} [CommRing R] (s : Set R) :

s ⊆ ↑(PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus s))

source

theorem PrimeSpectrum.le_vanishingIdeal_zeroLocus {R : Type u} [CommRing R] (I : Ideal R) :

I ≤ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I)

source

@[simp]

theorem PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical {R : Type u} [CommRing R] (I : Ideal R) :

PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I) = Ideal.radical I

source

@[simp]

theorem PrimeSpectrum.zeroLocus_radical {R : Type u} [CommRing R] (I : Ideal R) :

PrimeSpectrum.zeroLocus ↑(Ideal.radical I) = PrimeSpectrum.zeroLocus ↑I

source

theorem PrimeSpectrum.subset_zeroLocus_vanishingIdeal {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) :

t ⊆ PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t)

source

theorem PrimeSpectrum.zeroLocus_anti_mono {R : Type u} [CommRing R] {s : Set R} {t : Set R} (h : s ⊆ t) :

PrimeSpectrum.zeroLocus t ⊆ PrimeSpectrum.zeroLocus s

source

theorem PrimeSpectrum.zeroLocus_anti_mono_ideal {R : Type u} [CommRing R] {s : Ideal R} {t : Ideal R} (h : s ≤ t) :

PrimeSpectrum.zeroLocus ↑t ⊆ PrimeSpectrum.zeroLocus ↑s

source

theorem PrimeSpectrum.vanishingIdeal_anti_mono {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} {t : Set (PrimeSpectrum R)} (h : s ⊆ t) :

PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s

source

theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_iff {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :

PrimeSpectrum.zeroLocus ↑I ⊆ PrimeSpectrum.zeroLocus ↑J ↔ J ≤ Ideal.radical I

source

theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff {R : Type u} [CommRing R] (f : R) (g : R) :

PrimeSpectrum.zeroLocus {f} ⊆ PrimeSpectrum.zeroLocus {g} ↔ g ∈ Ideal.radical (Ideal.span {f})

source

theorem PrimeSpectrum.zeroLocus_bot {R : Type u} [CommRing R] :

PrimeSpectrum.zeroLocus ↑⊥ = Set.univ

source

@[simp]

theorem PrimeSpectrum.zeroLocus_singleton_zero {R : Type u} [CommRing R] :

PrimeSpectrum.zeroLocus {0} = Set.univ

source

@[simp]

theorem PrimeSpectrum.zeroLocus_empty {R : Type u} [CommRing R] :

PrimeSpectrum.zeroLocus ∅ = Set.univ

source

@[simp]

theorem PrimeSpectrum.vanishingIdeal_univ {R : Type u} [CommRing R] :

PrimeSpectrum.vanishingIdeal ∅ = ⊤

source

theorem PrimeSpectrum.zeroLocus_empty_of_one_mem {R : Type u} [CommRing R] {s : Set R} (h : 1 ∈ s) :

PrimeSpectrum.zeroLocus s = ∅

source

@[simp]

theorem PrimeSpectrum.zeroLocus_singleton_one {R : Type u} [CommRing R] :

PrimeSpectrum.zeroLocus {1} = ∅

source

theorem PrimeSpectrum.zeroLocus_empty_iff_eq_top {R : Type u} [CommRing R] {I : Ideal R} :

PrimeSpectrum.zeroLocus ↑I = ∅ ↔ I = ⊤

source

@[simp]

theorem PrimeSpectrum.zeroLocus_univ {R : Type u} [CommRing R] :

PrimeSpectrum.zeroLocus Set.univ = ∅

source

theorem PrimeSpectrum.vanishingIdeal_eq_top_iff {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} :

PrimeSpectrum.vanishingIdeal s = ⊤ ↔ s = ∅

source

theorem PrimeSpectrum.zeroLocus_sup {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :

PrimeSpectrum.zeroLocus ↑(I ⊔ J) = PrimeSpectrum.zeroLocus ↑I ∩ PrimeSpectrum.zeroLocus ↑J

source

theorem PrimeSpectrum.zeroLocus_union {R : Type u} [CommRing R] (s : Set R) (s' : Set R) :

PrimeSpectrum.zeroLocus (s ∪ s') = PrimeSpectrum.zeroLocus s ∩ PrimeSpectrum.zeroLocus s'

source

theorem PrimeSpectrum.vanishingIdeal_union {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) (t' : Set (PrimeSpectrum R)) :

PrimeSpectrum.vanishingIdeal (t ∪ t') = PrimeSpectrum.vanishingIdeal t ⊓ PrimeSpectrum.vanishingIdeal t'

source

theorem PrimeSpectrum.zeroLocus_iSup {R : Type u} [CommRing R] {ι : Sort u_1} (I : ι → Ideal R) :

PrimeSpectrum.zeroLocus ↑(⨆ (i : ι), I i) = ⋂ (i : ι), PrimeSpectrum.zeroLocus ↑(I i)

source

theorem PrimeSpectrum.zeroLocus_iUnion {R : Type u} [CommRing R] {ι : Sort u_1} (s : ι → Set R) :

PrimeSpectrum.zeroLocus (⋃ (i : ι), s i) = ⋂ (i : ι), PrimeSpectrum.zeroLocus (s i)

source

theorem PrimeSpectrum.zeroLocus_bUnion {R : Type u} [CommRing R] (s : Set (Set R)) :

PrimeSpectrum.zeroLocus (⋃ (s' : Set R) (_ : s' ∈ s), s') = ⋂ (s' : Set R) (_ : s' ∈ s), PrimeSpectrum.zeroLocus s'

source

theorem PrimeSpectrum.vanishingIdeal_iUnion {R : Type u} [CommRing R] {ι : Sort u_1} (t : ι → Set (PrimeSpectrum R)) :

PrimeSpectrum.vanishingIdeal (⋃ (i : ι), t i) = ⨅ (i : ι), PrimeSpectrum.vanishingIdeal (t i)

source

theorem PrimeSpectrum.zeroLocus_inf {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :

PrimeSpectrum.zeroLocus ↑(I ⊓ J) = PrimeSpectrum.zeroLocus ↑I ∪ PrimeSpectrum.zeroLocus ↑J

source

theorem PrimeSpectrum.union_zeroLocus {R : Type u} [CommRing R] (s : Set R) (s' : Set R) :

PrimeSpectrum.zeroLocus s ∪ PrimeSpectrum.zeroLocus s' = PrimeSpectrum.zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')

source

theorem PrimeSpectrum.zeroLocus_mul {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) :

PrimeSpectrum.zeroLocus ↑(I * J) = PrimeSpectrum.zeroLocus ↑I ∪ PrimeSpectrum.zeroLocus ↑J

source

theorem PrimeSpectrum.zeroLocus_singleton_mul {R : Type u} [CommRing R] (f : R) (g : R) :

PrimeSpectrum.zeroLocus {f * g} = PrimeSpectrum.zeroLocus {f} ∪ PrimeSpectrum.zeroLocus {g}

source

@[simp]

theorem PrimeSpectrum.zeroLocus_pow {R : Type u} [CommRing R] (I : Ideal R) {n : ℕ} (hn : 0 < n) :

PrimeSpectrum.zeroLocus ↑(I ^ n) = PrimeSpectrum.zeroLocus ↑I

source

@[simp]

theorem PrimeSpectrum.zeroLocus_singleton_pow {R : Type u} [CommRing R] (f : R) (n : ℕ) (hn : 0 < n) :

PrimeSpectrum.zeroLocus {f ^ n} = PrimeSpectrum.zeroLocus {f}

source

theorem PrimeSpectrum.sup_vanishingIdeal_le {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) (t' : Set (PrimeSpectrum R)) :

PrimeSpectrum.vanishingIdeal t ⊔ PrimeSpectrum.vanishingIdeal t' ≤ PrimeSpectrum.vanishingIdeal (t ∩ t')

source

theorem PrimeSpectrum.mem_compl_zeroLocus_iff_not_mem {R : Type u} [CommRing R] {f : R} {I : PrimeSpectrum R} :

I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ ↔ ¬f ∈ I.asIdeal

source

instance PrimeSpectrum.zariskiTopology {R : Type u} [CommRing R] :

TopologicalSpace (PrimeSpectrum 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.

source

theorem PrimeSpectrum.isOpen_iff {R : Type u} [CommRing R] (U : Set (PrimeSpectrum R)) :

IsOpen U ↔ ∃ s, Uᶜ = PrimeSpectrum.zeroLocus s

source

theorem PrimeSpectrum.isClosed_iff_zeroLocus {R : Type u} [CommRing R] (Z : Set (PrimeSpectrum R)) :

IsClosed Z ↔ ∃ s, Z = PrimeSpectrum.zeroLocus s

source

theorem PrimeSpectrum.isClosed_iff_zeroLocus_ideal {R : Type u} [CommRing R] (Z : Set (PrimeSpectrum R)) :

IsClosed Z ↔ ∃ I, Z = PrimeSpectrum.zeroLocus ↑I

source

theorem PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal {R : Type u} [CommRing R] (Z : Set (PrimeSpectrum R)) :

IsClosed Z ↔ ∃ I, Ideal.IsRadical I ∧ Z = PrimeSpectrum.zeroLocus ↑I

source

theorem PrimeSpectrum.isClosed_zeroLocus {R : Type u} [CommRing R] (s : Set R) :

IsClosed (PrimeSpectrum.zeroLocus s)

source

theorem PrimeSpectrum.isClosed_singleton_iff_isMaximal {R : Type u} [CommRing R] (x : PrimeSpectrum R) :

IsClosed {x} ↔ Ideal.IsMaximal x.asIdeal

source

theorem PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) :

PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t) = closure t

source

theorem PrimeSpectrum.vanishingIdeal_closure {R : Type u} [CommRing R] (t : Set (PrimeSpectrum R)) :

PrimeSpectrum.vanishingIdeal (closure t) = PrimeSpectrum.vanishingIdeal t

source

theorem PrimeSpectrum.closure_singleton {R : Type u} [CommRing R] (x : PrimeSpectrum R) :

closure {x} = PrimeSpectrum.zeroLocus ↑x.asIdeal

source

theorem PrimeSpectrum.isRadical_vanishingIdeal {R : Type u} [CommRing R] (s : Set (PrimeSpectrum R)) :

Ideal.IsRadical (PrimeSpectrum.vanishingIdeal s)

source

theorem PrimeSpectrum.vanishingIdeal_anti_mono_iff {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} {t : Set (PrimeSpectrum R)} (ht : IsClosed t) :

s ⊆ t ↔ PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s

source

theorem PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} {t : Set (PrimeSpectrum R)} (hs : IsClosed s) (ht : IsClosed t) :

s ⊂ t ↔ PrimeSpectrum.vanishingIdeal t < PrimeSpectrum.vanishingIdeal s

source

def PrimeSpectrum.closedsEmbedding (R : Type u_1) [CommRing R] :

(TopologicalSpace.Closeds (PrimeSpectrum R))ᵒᵈ ↪o Ideal R

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

Instances For

source

theorem PrimeSpectrum.t1Space_iff_isField {R : Type u} [CommRing R] [IsDomain R] :

T1Space (PrimeSpectrum R) ↔ IsField R

source

theorem PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical {R : Type u} [CommRing R] (I : Ideal R) (hI : Ideal.IsRadical I) :

IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ Ideal.IsPrime I

source

theorem PrimeSpectrum.isIrreducible_zeroLocus_iff {R : Type u} [CommRing R] (I : Ideal R) :

IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ Ideal.IsPrime (Ideal.radical I)

source

theorem PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} :

IsIrreducible s ↔ Ideal.IsPrime (PrimeSpectrum.vanishingIdeal s)

source

instance PrimeSpectrum.irreducibleSpace {R : Type u} [CommRing R] [IsDomain R] :

IrreducibleSpace (PrimeSpectrum R)

source

instance PrimeSpectrum.quasiSober {R : Type u} [CommRing R] :

QuasiSober (PrimeSpectrum R)

source

theorem PrimeSpectrum.preimage_comap_zeroLocus_aux {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) :

(fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (↑f '' s)

source

def PrimeSpectrum.comap {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) :

C(PrimeSpectrum S, PrimeSpectrum R)

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

Instances For

source

@[simp]

theorem PrimeSpectrum.comap_asIdeal {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (y : PrimeSpectrum S) :

(↑(PrimeSpectrum.comap f) y).asIdeal = Ideal.comap f y.asIdeal

source

@[simp]

theorem PrimeSpectrum.comap_id {R : Type u} [CommRing R] :

PrimeSpectrum.comap (RingHom.id R) = ContinuousMap.id (PrimeSpectrum R)

source

@[simp]

theorem PrimeSpectrum.comap_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] {S' : Type u_1} [CommRing S'] (f : R →+* S) (g : S →+* S') :

PrimeSpectrum.comap (RingHom.comp g f) = ContinuousMap.comp (PrimeSpectrum.comap f) (PrimeSpectrum.comap g)

source

theorem PrimeSpectrum.comap_comp_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] {S' : Type u_1} [CommRing S'] (f : R →+* S) (g : S →+* S') (x : PrimeSpectrum S') :

↑(PrimeSpectrum.comap (RingHom.comp g f)) x = ↑(PrimeSpectrum.comap f) (↑(PrimeSpectrum.comap g) x)

source

@[simp]

theorem PrimeSpectrum.preimage_comap_zeroLocus {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) :

↑(PrimeSpectrum.comap f) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (↑f '' s)

source

theorem PrimeSpectrum.comap_injective_of_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) :

Function.Injective ↑(PrimeSpectrum.comap f)

source

theorem PrimeSpectrum.comap_singleton_isClosed_of_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) (x : PrimeSpectrum S) (hx : IsClosed {x}) :

IsClosed {↑(PrimeSpectrum.comap f) x}

source

theorem PrimeSpectrum.comap_singleton_isClosed_of_isIntegral {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : RingHom.IsIntegral f) (x : PrimeSpectrum S) (hx : IsClosed {x}) :

IsClosed {↑(PrimeSpectrum.comap f) x}

source

theorem PrimeSpectrum.localization_comap_inducing {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] :

Inducing ↑(PrimeSpectrum.comap (algebraMap R S))

source

theorem PrimeSpectrum.localization_comap_injective {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] :

Function.Injective ↑(PrimeSpectrum.comap (algebraMap R S))

source

theorem PrimeSpectrum.localization_comap_embedding {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] :

Embedding ↑(PrimeSpectrum.comap (algebraMap R S))

source

theorem PrimeSpectrum.localization_comap_range {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] :

Set.range ↑(PrimeSpectrum.comap (algebraMap R S)) = {p | Disjoint ↑M ↑p.asIdeal}

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

source

theorem PrimeSpectrum.comap_inducing_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) :

Inducing ↑(PrimeSpectrum.comap f)

source

theorem PrimeSpectrum.image_comap_zeroLocus_eq_zeroLocus_comap {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) (I : Ideal S) :

↑(PrimeSpectrum.comap f) '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)

source

theorem PrimeSpectrum.range_comap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) :

Set.range ↑(PrimeSpectrum.comap f) = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)

source

theorem PrimeSpectrum.isClosed_range_comap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) :

IsClosed (Set.range ↑(PrimeSpectrum.comap f))

source

theorem PrimeSpectrum.closedEmbedding_comap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ↑f) :

ClosedEmbedding ↑(PrimeSpectrum.comap f)

source

def PrimeSpectrum.basicOpen {R : Type u} [CommRing R] (r : R) :

TopologicalSpace.Opens (PrimeSpectrum R)

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

Instances For

source

@[simp]

theorem PrimeSpectrum.mem_basicOpen {R : Type u} [CommRing R] (f : R) (x : PrimeSpectrum R) :

x ∈ PrimeSpectrum.basicOpen f ↔ ¬f ∈ x.asIdeal

source

theorem PrimeSpectrum.isOpen_basicOpen {R : Type u} [CommRing R] {a : R} :

IsOpen ↑(PrimeSpectrum.basicOpen a)

source

@[simp]

theorem PrimeSpectrum.basicOpen_eq_zeroLocus_compl {R : Type u} [CommRing R] (r : R) :

↑(PrimeSpectrum.basicOpen r) = (PrimeSpectrum.zeroLocus {r})ᶜ

source

@[simp]

theorem PrimeSpectrum.basicOpen_one {R : Type u} [CommRing R] :

PrimeSpectrum.basicOpen 1 = ⊤

source

@[simp]

theorem PrimeSpectrum.basicOpen_zero {R : Type u} [CommRing R] :

PrimeSpectrum.basicOpen 0 = ⊥

source

theorem PrimeSpectrum.basicOpen_le_basicOpen_iff {R : Type u} [CommRing R] (f : R) (g : R) :

PrimeSpectrum.basicOpen f ≤ PrimeSpectrum.basicOpen g ↔ f ∈ Ideal.radical (Ideal.span {g})

source

theorem PrimeSpectrum.basicOpen_mul {R : Type u} [CommRing R] (f : R) (g : R) :

PrimeSpectrum.basicOpen (f * g) = PrimeSpectrum.basicOpen f ⊓ PrimeSpectrum.basicOpen g

source

theorem PrimeSpectrum.basicOpen_mul_le_left {R : Type u} [CommRing R] (f : R) (g : R) :

PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen f

source

theorem PrimeSpectrum.basicOpen_mul_le_right {R : Type u} [CommRing R] (f : R) (g : R) :

PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen g

source

@[simp]

theorem PrimeSpectrum.basicOpen_pow {R : Type u} [CommRing R] (f : R) (n : ℕ) (hn : 0 < n) :

PrimeSpectrum.basicOpen (f ^ n) = PrimeSpectrum.basicOpen f

source

theorem PrimeSpectrum.isTopologicalBasis_basic_opens {R : Type u} [CommRing R] :

TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(PrimeSpectrum.basicOpen r))

source

theorem PrimeSpectrum.isBasis_basic_opens {R : Type u} [CommRing R] :

TopologicalSpace.Opens.IsBasis (Set.range PrimeSpectrum.basicOpen)

source

theorem PrimeSpectrum.isCompact_basicOpen {R : Type u} [CommRing R] (f : R) :

IsCompact ↑(PrimeSpectrum.basicOpen f)

source

@[simp]

theorem PrimeSpectrum.basicOpen_eq_bot_iff {R : Type u} [CommRing R] (f : R) :

PrimeSpectrum.basicOpen f = ⊥ ↔ IsNilpotent f

source

theorem PrimeSpectrum.localization_away_comap_range {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] :

Set.range ↑(PrimeSpectrum.comap (algebraMap R S)) = ↑(PrimeSpectrum.basicOpen r)

source

theorem PrimeSpectrum.localization_away_openEmbedding {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] :

OpenEmbedding ↑(PrimeSpectrum.comap (algebraMap R S))

source

instance PrimeSpectrum.compactSpace {R : Type u} [CommRing R] :

CompactSpace (PrimeSpectrum R)

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

The specialization order #

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

source

instance PrimeSpectrum.instPartialOrderPrimeSpectrum {R : Type u} [CommRing R] :

PartialOrder (PrimeSpectrum R)

source

@[simp]

theorem PrimeSpectrum.asIdeal_le_asIdeal {R : Type u} [CommRing R] (x : PrimeSpectrum R) (y : PrimeSpectrum R) :

x.asIdeal ≤ y.asIdeal ↔ x ≤ y

source

@[simp]

theorem PrimeSpectrum.asIdeal_lt_asIdeal {R : Type u} [CommRing R] (x : PrimeSpectrum R) (y : PrimeSpectrum R) :

x.asIdeal < y.asIdeal ↔ x < y

source

theorem PrimeSpectrum.le_iff_mem_closure {R : Type u} [CommRing R] (x : PrimeSpectrum R) (y : PrimeSpectrum R) :

x ≤ y ↔ y ∈ closure {x}

source

theorem PrimeSpectrum.le_iff_specializes {R : Type u} [CommRing R] (x : PrimeSpectrum R) (y : PrimeSpectrum R) :

x ≤ y ↔ x ⤳ y

source

@[simp]

theorem PrimeSpectrum.nhdsOrderEmbedding_apply {R : Type u} [CommRing R] (a : PrimeSpectrum R) :

↑PrimeSpectrum.nhdsOrderEmbedding a = nhds a

source

def PrimeSpectrum.nhdsOrderEmbedding {R : Type u} [CommRing R] :

PrimeSpectrum R ↪o Filter (PrimeSpectrum R)

nhds as an order embedding.

Instances For

source

instance PrimeSpectrum.instT0SpacePrimeSpectrumZariskiTopology {R : Type u} [CommRing R] :

T0Space (PrimeSpectrum R)

source

instance PrimeSpectrum.instOrderBotPrimeSpectrumToLEToPreorderInstPartialOrderPrimeSpectrum {R : Type u} [CommRing R] [IsDomain R] :

OrderBot (PrimeSpectrum R)

source

instance PrimeSpectrum.instUniquePrimeSpectrumToCommRingToEuclideanDomain {R : Type u_1} [Field R] :

Unique (PrimeSpectrum R)

source

def PrimeSpectrum.localizationMapOfSpecializes {R : Type u} [CommRing R] {x : PrimeSpectrum R} {y : PrimeSpectrum R} (h : x ⤳ y) :

Localization.AtPrime y.asIdeal →+* Localization.AtPrime x.asIdeal

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

Instances For

source

def LocalRing.closedPoint (R : Type u) [CommRing R] [LocalRing R] :

PrimeSpectrum R

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

Instances For

source

theorem LocalRing.isLocalRingHom_iff_comap_closedPoint {R : Type u} [CommRing R] [LocalRing R] {S : Type v} [CommRing S] [LocalRing S] (f : R →+* S) :

IsLocalRingHom f ↔ ↑(PrimeSpectrum.comap f) (LocalRing.closedPoint S) = LocalRing.closedPoint R

source

@[simp]

theorem LocalRing.comap_closedPoint {R : Type u} [CommRing R] [LocalRing R] {S : Type v} [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalRingHom f] :

↑(PrimeSpectrum.comap f) (LocalRing.closedPoint S) = LocalRing.closedPoint R

source

theorem LocalRing.specializes_closedPoint {R : Type u} [CommRing R] [LocalRing R] (x : PrimeSpectrum R) :

x ⤳ LocalRing.closedPoint R

source

theorem LocalRing.closedPoint_mem_iff {R : Type u} [CommRing R] [LocalRing R] (U : TopologicalSpace.Opens (PrimeSpectrum R)) :

LocalRing.closedPoint R ∈ U ↔ U = ⊤

source

@[simp]

theorem LocalRing.PrimeSpectrum.comap_residue {R : Type u} [CommRing R] [LocalRing R] (x : PrimeSpectrum (LocalRing.ResidueField R)) :

↑(PrimeSpectrum.comap (LocalRing.residue R)) x = LocalRing.closedPoint R