algebraic_geometry.prime_spectrum.basic

@[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

prime_spectrum R = {I // I.is_prime}

source

def prime_spectrum.as_ideal {R : Type u} [comm_ring R] (x : prime_spectrum R) :

ideal R

A method to view a point in the prime spectrum of a commutative ring as an ideal of that ring.

source

@[protected, instance]

def prime_spectrum.is_prime {R : Type u} [comm_ring R] (x : prime_spectrum R) :

x.as_ideal.is_prime

source

theorem prime_spectrum.punit (x : prime_spectrum punit) :

false

The prime spectrum of the zero ring is empty.

source

noncomputable def prime_spectrum.prime_spectrum_prod (R : Type u) [comm_ring R] (S : Type v) [comm_ring S] :

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

prime_spectrum.prime_spectrum_prod R S = ideal.prime_ideals_equiv R S

source

@[simp]

theorem prime_spectrum.prime_spectrum_prod_symm_inl_as_ideal {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (x : prime_spectrum R) :

(⇑((prime_spectrum.prime_spectrum_prod R S).symm) (sum.inl x)).as_ideal = x.as_ideal.prod ⊤

source

@[simp]

theorem prime_spectrum.prime_spectrum_prod_symm_inr_as_ideal {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (x : prime_spectrum S) :

(⇑((prime_spectrum.prime_spectrum_prod R S).symm) (sum.inr x)).as_ideal = ⊤.prod x.as_ideal

source

@[ext]

theorem prime_spectrum.ext {R : Type u} [comm_ring R] {x y : prime_spectrum R} :

x = y ↔ x.as_ideal = y.as_ideal

source

def prime_spectrum.zero_locus {R : Type u} [comm_ring R] (s : set R) :

set (prime_spectrum 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

prime_spectrum.zero_locus s = {x : prime_spectrum R | s ⊆ ↑(x.as_ideal)}

source

@[simp]

theorem prime_spectrum.mem_zero_locus {R : Type u} [comm_ring R] (x : prime_spectrum R) (s : set R) :

x ∈ prime_spectrum.zero_locus s ↔ s ⊆ ↑(x.as_ideal)

source

@[simp]

theorem prime_spectrum.zero_locus_span {R : Type u} [comm_ring R] (s : set R) :

prime_spectrum.zero_locus ↑(ideal.span s) = prime_spectrum.zero_locus s

source

def prime_spectrum.vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum 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, vanishing_ideal t is exactly the ideal of R consisting of all "functions" that vanish on all of t.

Equations

prime_spectrum.vanishing_ideal t = ⨅ (x : prime_spectrum R) (h : x ∈ t), x.as_ideal

source

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 ∈ t → f ∈ x.as_ideal}

source

theorem prime_spectrum.mem_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) (f : R) :

f ∈ prime_spectrum.vanishing_ideal t ↔ ∀ (x : prime_spectrum R), x ∈ t → f ∈ x.as_ideal

source

@[simp]

theorem prime_spectrum.vanishing_ideal_singleton {R : Type u} [comm_ring R] (x : prime_spectrum R) :

prime_spectrum.vanishing_ideal {x} = x.as_ideal

source

theorem prime_spectrum.subset_zero_locus_iff_le_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) (I : ideal R) :

t ⊆ prime_spectrum.zero_locus ↑I ↔ I ≤ prime_spectrum.vanishing_ideal t

source

theorem prime_spectrum.gc (R : Type u) [comm_ring R] :

galois_connection (λ (I : ideal R), prime_spectrum.zero_locus ↑I) (λ (t : order_dual (set (prime_spectrum R))), prime_spectrum.vanishing_ideal t)

zero_locus and vanishing_ideal form a galois connection.

source

theorem prime_spectrum.gc_set (R : Type u) [comm_ring R] :

galois_connection (λ (s : set R), prime_spectrum.zero_locus s) (λ (t : order_dual (set (prime_spectrum R))), ↑(prime_spectrum.vanishing_ideal t))

zero_locus and vanishing_ideal form a galois connection.

source

theorem prime_spectrum.subset_zero_locus_iff_subset_vanishing_ideal (R : Type u) [comm_ring R] (t : set (prime_spectrum R)) (s : set R) :

t ⊆ prime_spectrum.zero_locus s ↔ s ⊆ ↑(prime_spectrum.vanishing_ideal t)

source

theorem prime_spectrum.subset_vanishing_ideal_zero_locus {R : Type u} [comm_ring R] (s : set R) :

s ⊆ ↑(prime_spectrum.vanishing_ideal (prime_spectrum.zero_locus s))

source

theorem prime_spectrum.le_vanishing_ideal_zero_locus {R : Type u} [comm_ring R] (I : ideal R) :

I ≤ prime_spectrum.vanishing_ideal (prime_spectrum.zero_locus ↑I)

source

@[simp]

theorem prime_spectrum.vanishing_ideal_zero_locus_eq_radical {R : Type u} [comm_ring R] (I : ideal R) :

prime_spectrum.vanishing_ideal (prime_spectrum.zero_locus ↑I) = I.radical

source

@[simp]

theorem prime_spectrum.zero_locus_radical {R : Type u} [comm_ring R] (I : ideal R) :

prime_spectrum.zero_locus ↑(I.radical) = prime_spectrum.zero_locus ↑I

source

theorem prime_spectrum.subset_zero_locus_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) :

t ⊆ prime_spectrum.zero_locus ↑(prime_spectrum.vanishing_ideal t)

source

theorem prime_spectrum.zero_locus_anti_mono {R : Type u} [comm_ring R] {s t : set R} (h : s ⊆ t) :

prime_spectrum.zero_locus t ⊆ prime_spectrum.zero_locus s

source

theorem prime_spectrum.zero_locus_anti_mono_ideal {R : Type u} [comm_ring R] {s t : ideal R} (h : s ≤ t) :

prime_spectrum.zero_locus ↑t ⊆ prime_spectrum.zero_locus ↑s

source

theorem prime_spectrum.vanishing_ideal_anti_mono {R : Type u} [comm_ring R] {s t : set (prime_spectrum R)} (h : s ⊆ t) :

prime_spectrum.vanishing_ideal t ≤ prime_spectrum.vanishing_ideal s

source

theorem prime_spectrum.zero_locus_subset_zero_locus_iff {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus ↑I ⊆ prime_spectrum.zero_locus ↑J ↔ J ≤ I.radical

source

theorem prime_spectrum.zero_locus_subset_zero_locus_singleton_iff {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.zero_locus {f} ⊆ prime_spectrum.zero_locus {g} ↔ g ∈ (ideal.span {f}).radical

source

theorem prime_spectrum.zero_locus_bot {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus ↑⊥ = set.univ

source

@[simp]

theorem prime_spectrum.zero_locus_singleton_zero {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus {0} = set.univ

source

@[simp]

theorem prime_spectrum.zero_locus_empty {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus ∅ = set.univ

source

@[simp]

theorem prime_spectrum.vanishing_ideal_univ {R : Type u} [comm_ring R] :

prime_spectrum.vanishing_ideal ∅ = ⊤

source

theorem prime_spectrum.zero_locus_empty_of_one_mem {R : Type u} [comm_ring R] {s : set R} (h : 1 ∈ s) :

prime_spectrum.zero_locus s = ∅

source

@[simp]

theorem prime_spectrum.zero_locus_singleton_one {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus {1} = ∅

source

theorem prime_spectrum.zero_locus_empty_iff_eq_top {R : Type u} [comm_ring R] {I : ideal R} :

prime_spectrum.zero_locus ↑I = ∅ ↔ I = ⊤

source

@[simp]

theorem prime_spectrum.zero_locus_univ {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus set.univ = ∅

source

theorem prime_spectrum.zero_locus_sup {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus ↑(I ⊔ J) = prime_spectrum.zero_locus ↑I ∩ prime_spectrum.zero_locus ↑J

source

theorem prime_spectrum.zero_locus_union {R : Type u} [comm_ring R] (s s' : set R) :

prime_spectrum.zero_locus (s ∪ s') = prime_spectrum.zero_locus s ∩ prime_spectrum.zero_locus s'

source

theorem prime_spectrum.vanishing_ideal_union {R : Type u} [comm_ring R] (t t' : set (prime_spectrum R)) :

prime_spectrum.vanishing_ideal (t ∪ t') = prime_spectrum.vanishing_ideal t ⊓ prime_spectrum.vanishing_ideal t'

source

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)

source

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)

source

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'

source

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)

source

theorem prime_spectrum.zero_locus_inf {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus ↑(I ⊓ J) = prime_spectrum.zero_locus ↑I ∪ prime_spectrum.zero_locus ↑J

source

theorem prime_spectrum.union_zero_locus {R : Type u} [comm_ring R] (s s' : set R) :

prime_spectrum.zero_locus s ∪ prime_spectrum.zero_locus s' = prime_spectrum.zero_locus ↑(ideal.span s ⊓ ideal.span s')

source

theorem prime_spectrum.zero_locus_mul {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus (↑I * J) = prime_spectrum.zero_locus ↑I ∪ prime_spectrum.zero_locus ↑J

source

theorem prime_spectrum.zero_locus_singleton_mul {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.zero_locus {f * g} = prime_spectrum.zero_locus {f} ∪ prime_spectrum.zero_locus {g}

source

@[simp]

theorem prime_spectrum.zero_locus_pow {R : Type u} [comm_ring R] (I : ideal R) {n : ℕ} (hn : 0 < n) :

prime_spectrum.zero_locus ↑(I ^ n) = prime_spectrum.zero_locus ↑I

source

@[simp]

theorem prime_spectrum.zero_locus_singleton_pow {R : Type u} [comm_ring R] (f : R) (n : ℕ) (hn : 0 < n) :

prime_spectrum.zero_locus {f ^ n} = prime_spectrum.zero_locus {f}

source

theorem prime_spectrum.sup_vanishing_ideal_le {R : Type u} [comm_ring R] (t t' : set (prime_spectrum R)) :

prime_spectrum.vanishing_ideal t ⊔ prime_spectrum.vanishing_ideal t' ≤ prime_spectrum.vanishing_ideal (t ∩ t')

source

theorem prime_spectrum.mem_compl_zero_locus_iff_not_mem {R : Type u} [comm_ring R] {f : R} {I : prime_spectrum R} :

I ∈ (prime_spectrum.zero_locus {f})ᶜ ↔ f ∉ I.as_ideal

source

@[protected, instance]

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

topological_space (prime_spectrum 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

prime_spectrum.zariski_topology = topological_space.of_closed (set.range prime_spectrum.zero_locus) prime_spectrum.zariski_topology._proof_1 prime_spectrum.zariski_topology._proof_2 prime_spectrum.zariski_topology._proof_3

source

theorem prime_spectrum.is_open_iff {R : Type u} [comm_ring R] (U : set (prime_spectrum R)) :

is_open U ↔ ∃ (s : set R), Uᶜ = prime_spectrum.zero_locus s

source

theorem prime_spectrum.is_closed_iff_zero_locus {R : Type u} [comm_ring R] (Z : set (prime_spectrum R)) :

is_closed Z ↔ ∃ (s : set R), Z = prime_spectrum.zero_locus s

source

theorem prime_spectrum.is_closed_iff_zero_locus_ideal {R : Type u} [comm_ring R] (Z : set (prime_spectrum R)) :

is_closed Z ↔ ∃ (s : ideal R), Z = prime_spectrum.zero_locus ↑s

source

theorem prime_spectrum.is_closed_iff_zero_locus_radical_ideal {R : Type u} [comm_ring R] (Z : set (prime_spectrum R)) :

is_closed Z ↔ ∃ (s : ideal R), s.radical = s ∧ Z = prime_spectrum.zero_locus ↑s

source

theorem prime_spectrum.is_closed_zero_locus {R : Type u} [comm_ring R] (s : set R) :

is_closed (prime_spectrum.zero_locus s)

source

theorem prime_spectrum.is_closed_singleton_iff_is_maximal {R : Type u} [comm_ring R] (x : prime_spectrum R) :

is_closed {x} ↔ x.as_ideal.is_maximal

source

theorem prime_spectrum.zero_locus_vanishing_ideal_eq_closure {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) :

prime_spectrum.zero_locus ↑(prime_spectrum.vanishing_ideal t) = closure t

source

theorem prime_spectrum.vanishing_ideal_closure {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) :

prime_spectrum.vanishing_ideal (closure t) = prime_spectrum.vanishing_ideal t

source

theorem prime_spectrum.t1_space_iff_is_field {R : Type u} [comm_ring R] [is_domain R] :

t1_space (prime_spectrum R) ↔ is_field R

source

theorem prime_spectrum.is_irreducible_zero_locus_iff_of_radical {R : Type u} [comm_ring R] (I : ideal R) (hI : I.radical = I) :

is_irreducible (prime_spectrum.zero_locus ↑I) ↔ I.is_prime

source

theorem prime_spectrum.is_irreducible_zero_locus_iff {R : Type u} [comm_ring R] (I : ideal R) :

is_irreducible (prime_spectrum.zero_locus ↑I) ↔ I.radical.is_prime

source

@[protected, instance]

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

irreducible_space (prime_spectrum R)

source

@[protected, instance]

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

quasi_sober (prime_spectrum R)

source

theorem prime_spectrum.preimage_comap_zero_locus_aux {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (s : set R) :

(λ (y : prime_spectrum S), ⟨ideal.comap f y.as_ideal, _⟩) ⁻¹' prime_spectrum.zero_locus s = prime_spectrum.zero_locus (⇑f '' s)

source

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

C(prime_spectrum S, prime_spectrum R)

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

Equations

prime_spectrum.comap f = {to_fun := λ (y : prime_spectrum S), ⟨ideal.comap f y.as_ideal, _⟩, continuous_to_fun := _}

source

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

(⇑(prime_spectrum.comap f) y).as_ideal = ideal.comap f y.as_ideal

source

@[simp]

theorem prime_spectrum.comap_id {R : Type u} [comm_ring R] :

prime_spectrum.comap (ring_hom.id R) = continuous_map.id (prime_spectrum R)

source

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

prime_spectrum.comap (g.comp f) = (prime_spectrum.comap f).comp (prime_spectrum.comap g)

source

theorem prime_spectrum.comap_comp_apply {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') (x : prime_spectrum S') :

⇑(prime_spectrum.comap (g.comp f)) x = ⇑(prime_spectrum.comap f) (⇑(prime_spectrum.comap g) x)

source

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

⇑(prime_spectrum.comap f) ⁻¹' prime_spectrum.zero_locus s = prime_spectrum.zero_locus (⇑f '' s)

source

theorem prime_spectrum.comap_injective_of_surjective {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) :

function.injective ⇑(prime_spectrum.comap f)

source

theorem prime_spectrum.comap_singleton_is_closed_of_surjective {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) (x : prime_spectrum S) (hx : is_closed {x}) :

is_closed {⇑(prime_spectrum.comap f) x}

source

theorem prime_spectrum.comap_singleton_is_closed_of_is_integral {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (hf : f.is_integral) (x : prime_spectrum S) (hx : is_closed {x}) :

is_closed {⇑(prime_spectrum.comap f) x}

source

theorem prime_spectrum.localization_comap_inducing {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [algebra R S] (M : submonoid R) [is_localization M S] :

inducing ⇑(prime_spectrum.comap (algebra_map R S))

source

theorem prime_spectrum.localization_comap_injective {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [algebra R S] (M : submonoid R) [is_localization M S] :

function.injective ⇑(prime_spectrum.comap (algebra_map R S))

source

theorem prime_spectrum.localization_comap_embedding {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [algebra R S] (M : submonoid R) [is_localization M S] :

embedding ⇑(prime_spectrum.comap (algebra_map R S))

source

theorem prime_spectrum.localization_comap_range {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [algebra R S] (M : submonoid R) [is_localization M S] :

set.range ⇑(prime_spectrum.comap (algebra_map R S)) = {p : prime_spectrum R | disjoint ↑M ↑(p.as_ideal)}

source

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

topological_space.opens (prime_spectrum R)

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

Equations

prime_spectrum.basic_open r = ⟨{x : prime_spectrum R | r ∉ x.as_ideal}, _⟩

source

@[simp]

theorem prime_spectrum.mem_basic_open {R : Type u} [comm_ring R] (f : R) (x : prime_spectrum R) :

x ∈ prime_spectrum.basic_open f ↔ f ∉ x.as_ideal

source

theorem prime_spectrum.is_open_basic_open {R : Type u} [comm_ring R] {a : R} :

is_open ↑(prime_spectrum.basic_open a)

source

@[simp]

theorem prime_spectrum.basic_open_eq_zero_locus_compl {R : Type u} [comm_ring R] (r : R) :

↑(prime_spectrum.basic_open r) = (prime_spectrum.zero_locus {r})ᶜ

source

@[simp]

theorem prime_spectrum.basic_open_one {R : Type u} [comm_ring R] :

prime_spectrum.basic_open 1 = ⊤

source

@[simp]

theorem prime_spectrum.basic_open_zero {R : Type u} [comm_ring R] :

prime_spectrum.basic_open 0 = ⊥

source

theorem prime_spectrum.basic_open_le_basic_open_iff {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open f ≤ prime_spectrum.basic_open g ↔ f ∈ (ideal.span {g}).radical

source

theorem prime_spectrum.basic_open_mul {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open (f * g) = prime_spectrum.basic_open f ⊓ prime_spectrum.basic_open g

source

theorem prime_spectrum.basic_open_mul_le_left {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open (f * g) ≤ prime_spectrum.basic_open f

source

theorem prime_spectrum.basic_open_mul_le_right {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open (f * g) ≤ prime_spectrum.basic_open g

source

@[simp]

theorem prime_spectrum.basic_open_pow {R : Type u} [comm_ring R] (f : R) (n : ℕ) (hn : 0 < n) :

prime_spectrum.basic_open (f ^ n) = prime_spectrum.basic_open f

source

theorem prime_spectrum.is_topological_basis_basic_opens {R : Type u} [comm_ring R] :

topological_space.is_topological_basis (set.range (λ (r : R), ↑(prime_spectrum.basic_open r)))

source

theorem prime_spectrum.is_basis_basic_opens {R : Type u} [comm_ring R] :

topological_space.opens.is_basis (set.range prime_spectrum.basic_open)

source

theorem prime_spectrum.is_compact_basic_open {R : Type u} [comm_ring R] (f : R) :

is_compact ↑(prime_spectrum.basic_open f)

source

@[simp]

theorem prime_spectrum.basic_open_eq_bot_iff {R : Type u} [comm_ring R] (f : R) :

prime_spectrum.basic_open f = ⊥ ↔ is_nilpotent f

source

theorem prime_spectrum.localization_away_comap_range {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [algebra R S] (r : R) [is_localization.away r S] :

set.range ⇑(prime_spectrum.comap (algebra_map R S)) = ↑(prime_spectrum.basic_open r)

source

theorem prime_spectrum.localization_away_open_embedding {R : Type u} [comm_ring R] (S : Type v) [comm_ring S] [algebra R S] (r : R) [is_localization.away r S] :

open_embedding ⇑(prime_spectrum.comap (algebra_map R S))

source

@[protected, instance]

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

compact_space (prime_spectrum R)

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

source

@[protected, instance]

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

partial_order (prime_spectrum R)

Equations

prime_spectrum.partial_order = subtype.partial_order (λ (I : ideal R), I.is_prime)

source

@[simp]

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

x.as_ideal ≤ y.as_ideal ↔ x ≤ y

source

@[simp]

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

x.as_ideal < y.as_ideal ↔ x < y

source

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

x ≤ y ↔ y ∈ closure {x}

source

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

x ≤ y ↔ x ⤳ y

source

@[protected, instance]

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

t0_space (prime_spectrum R)

source

noncomputable def prime_spectrum.localization_map_of_specializes {R : Type u} [comm_ring R] {x y : prime_spectrum R} (h : x ⤳ y) :

localization.at_prime y.as_ideal →+* localization.at_prime x.as_ideal

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

Equations

prime_spectrum.localization_map_of_specializes h = is_localization.lift _

source

def local_ring.closed_point (R : Type u) [comm_ring R] [local_ring R] :

prime_spectrum R

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

Equations

local_ring.closed_point R = ⟨local_ring.maximal_ideal R _inst_2, _⟩

source

theorem local_ring.is_local_ring_hom_iff_comap_closed_point {R : Type u} [comm_ring R] [local_ring R] {S : Type v} [comm_ring S] [local_ring S] (f : R →+* S) :

is_local_ring_hom f ↔ ⇑(prime_spectrum.comap f) (local_ring.closed_point S) = local_ring.closed_point R

source

@[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) [is_local_ring_hom f] :

⇑(prime_spectrum.comap f) (local_ring.closed_point S) = local_ring.closed_point R

mathlib documentation

Prime spectrum of a commutative ring #

Main definitions #

Conventions #

Inspiration/contributors #

The specialization order #