Maximal spectrum of a commutative ring #

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

The maximal spectrum of a commutative ring is the type of all maximal ideals. It is naturally a subset of the prime spectrum endowed with the subspace topology.

Main definitions #

maximal_spectrum R: The maximal spectrum of a commutative ring R, i.e., the set of all maximal ideals of R.

Implementation notes #

The Zariski topology on the maximal spectrum is defined as the subspace topology induced by the natural inclusion into the prime spectrum to avoid API duplication for zero loci.

source

theorem maximal_spectrum.ext {R : Type u} {_inst_1 : comm_ring R} (x y : maximal_spectrum R) (h : x.as_ideal = y.as_ideal) :

x = y

source

theorem maximal_spectrum.ext_iff {R : Type u} {_inst_1 : comm_ring R} (x y : maximal_spectrum R) :

x = y ↔ x.as_ideal = y.as_ideal

source

@[ext]

structure maximal_spectrum (R : Type u) [comm_ring R] :

Type u

as_ideal : ideal R
is_maximal : self.as_ideal.is_maximal

The maximal spectrum of a commutative ring R is the type of all maximal ideals of R.

Instances for maximal_spectrum

source

@[protected, instance]

def maximal_spectrum.nonempty {R : Type u} [comm_ring R] [nontrivial R] :

nonempty (maximal_spectrum R)

source

def maximal_spectrum.to_prime_spectrum {R : Type u} [comm_ring R] (x : maximal_spectrum R) :

prime_spectrum R

The natural inclusion from the maximal spectrum to the prime spectrum.

Equations

x.to_prime_spectrum = {as_ideal := x.as_ideal, is_prime := _}

source

theorem maximal_spectrum.to_prime_spectrum_injective {R : Type u} [comm_ring R] :

function.injective maximal_spectrum.to_prime_spectrum

source

theorem maximal_spectrum.to_prime_spectrum_range {R : Type u} [comm_ring R] :

set.range maximal_spectrum.to_prime_spectrum = {x : prime_spectrum R | is_closed {x}}

source

@[protected, instance]

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

topological_space (maximal_spectrum R)

The Zariski topology on the maximal spectrum of a commutative ring is defined as the subspace topology induced by the natural inclusion into the prime spectrum.

Equations

maximal_spectrum.zariski_topology = topological_space.induced maximal_spectrum.to_prime_spectrum prime_spectrum.zariski_topology

source

@[protected, instance]

def maximal_spectrum.t1_space {R : Type u} [comm_ring R] :

t1_space (maximal_spectrum R)

source

theorem maximal_spectrum.to_prime_spectrum_continuous {R : Type u} [comm_ring R] :

continuous maximal_spectrum.to_prime_spectrum

source

theorem maximal_spectrum.infi_localization_eq_bot (R : Type u) [comm_ring R] [is_domain R] (K : Type v) [field K] [algebra R K] [is_fraction_ring R K] :

(⨅ (v : maximal_spectrum R), localization.subalgebra.of_field K v.as_ideal.prime_compl _) = ⊥

An integral domain is equal to the intersection of its localizations at all its maximal ideals viewed as subalgebras of its field of fractions.

source

theorem prime_spectrum.infi_localization_eq_bot (R : Type u) [comm_ring R] [is_domain R] (K : Type v) [field K] [algebra R K] [is_fraction_ring R K] :

(⨅ (v : prime_spectrum R), localization.subalgebra.of_field K v.as_ideal.prime_compl _) = ⊥

An integral domain is equal to the intersection of its localizations at all its prime ideals viewed as subalgebras of its field of fractions.