Documentation

Mathlib.RingTheory.MaximalSpectrum

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 #

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 MaximalSpectrum.ext {R : Type u} :
∀ {inst : CommRing R} (x y : MaximalSpectrum R), x.asIdeal = y.asIdeal → x = y
source
theorem MaximalSpectrum.ext_iff {R : Type u} :
∀ {inst : CommRing R} (x y : MaximalSpectrum R), x = y ↔ x.asIdeal = y.asIdeal
source
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 : self.asIdeal.IsMaximal
Instances For
    source
    theorem MaximalSpectrum.IsMaximal {R : Type u} [CommRing R] (self : MaximalSpectrum R) :
    self.asIdeal.IsMaximal
    source
    instance MaximalSpectrum.instNonemptyOfNontrivial {R : Type u} [CommRing R] [Nontrivial R] :
    Nonempty (MaximalSpectrum R)
    Equations
    • ⋯ = ⋯
    source
    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
    • x.toPrimeSpectrum = { asIdeal := x.asIdeal, isPrime := ⋯ }
    Instances For
      source
      theorem MaximalSpectrum.toPrimeSpectrum_injective {R : Type u} [CommRing R] :
      Function.Injective MaximalSpectrum.toPrimeSpectrum
      source
      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 v.asIdeal.primeCompl ⋯ = ⊥

      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 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 v.asIdeal.primeCompl ⋯ = ⊥

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