Maximal spectrum of a commutative ring

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

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

theorem MaximalSpectrum.ext {R : Type u} : ∀ {inst : CommRing R} (x y : MaximalSpectrum R), x.asIdeal = y.asIdeal → x = y

theorem MaximalSpectrum.ext_iff {R : Type u} : ∀ {inst : CommRing R} (x y : MaximalSpectrum R), x = y ↔ x.asIdeal = y.asIdeal

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

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

• asIdeal : Ideal R
• IsMaximal : Ideal.IsMaximal self.asIdeal

instance MaximalSpectrum.instNonemptyMaximalSpectrum {R : Type u} [CommRing R] [Nontrivial R] : Nonempty (MaximalSpectrum R)

Equations

• (_ : Nonempty (MaximalSpectrum R)) = (_ : Nonempty (MaximalSpectrum R))

def MaximalSpectrum.toPrimeSpectrum {R : Type u} [CommRing R] (x : MaximalSpectrum R) : PrimeSpectrum R

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

Equations

• MaximalSpectrum.toPrimeSpectrum x = { asIdeal := x.asIdeal, IsPrime := (_ : Ideal.IsPrime x.asIdeal) }

theorem MaximalSpectrum.toPrimeSpectrum_injective {R : Type u} [CommRing R] : Function.Injective MaximalSpectrum.toPrimeSpectrum

theorem MaximalSpectrum.toPrimeSpectrum_range {R : Type u} [CommRing R] : Set.range MaximalSpectrum.toPrimeSpectrum = {x : PrimeSpectrum R | IsClosed {x}}

instance MaximalSpectrum.zariskiTopology {R : Type u} [CommRing R] : TopologicalSpace (MaximalSpectrum 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

• MaximalSpectrum.zariskiTopology = TopologicalSpace.induced MaximalSpectrum.toPrimeSpectrum PrimeSpectrum.zariskiTopology

instance MaximalSpectrum.instT1SpaceMaximalSpectrumZariskiTopology {R : Type u} [CommRing R] : T1Space (MaximalSpectrum R)

Equations

• (_ : T1Space (MaximalSpectrum R)) = (_ : T1Space (MaximalSpectrum R))

theorem MaximalSpectrum.toPrimeSpectrum_continuous {R : Type u} [CommRing R] : Continuous MaximalSpectrum.toPrimeSpectrum

theorem MaximalSpectrum.iInf_localization_eq_bot (R : Type u) [CommRing R] [IsDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : ⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal) (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) = ⊥

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

theorem PrimeSpectrum.iInf_localization_eq_bot (R : Type u) [CommRing R] [IsDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : ⨅ (v : PrimeSpectrum R), Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal) (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) = ⊥

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