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.

structure MaximalSpectrum (R : Type u_1) [CommSemiring R] : Type u_1

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

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

theorem MaximalSpectrum.ext {R : Type u_1} {inst✝ : CommSemiring R} {x y : MaximalSpectrum R} (asIdeal : x.asIdeal = y.asIdeal) : x = y

instance MaximalSpectrum.instNonemptyOfNontrivial {R : Type u_1} [CommSemiring R] [Nontrivial R] : Nonempty (MaximalSpectrum R)

def MaximalSpectrum.toPrimeSpectrum {R : Type u_1} [CommSemiring R] (x : MaximalSpectrum R) : PrimeSpectrum R

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

Equations

• x.toPrimeSpectrum = { asIdeal := x.asIdeal, isPrime := ⋯ }

theorem MaximalSpectrum.toPrimeSpectrum_injective {R : Type u_1} [CommSemiring R] : Function.Injective MaximalSpectrum.toPrimeSpectrum

theorem MaximalSpectrum.iInf_localization_eq_bot (R : Type u_4) [CommRing R] [IsDomain R] (K : Type u_5) [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.

theorem PrimeSpectrum.iInf_localization_eq_bot (R : Type u_4) [CommRing R] [IsDomain R] (K : Type u_5) [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.

@[reducible, inline]

abbrev MaximalSpectrum.PiLocalization (R : Type u_1) [CommSemiring R] : Type u_1

The product of localizations at all maximal ideals of a commutative semiring.

Equations

• MaximalSpectrum.PiLocalization R = ((I : MaximalSpectrum R) → Localization.AtPrime I.asIdeal)

def MaximalSpectrum.toPiLocalization (R : Type u_1) [CommSemiring R] : R →+* MaximalSpectrum.PiLocalization R

The canonical ring homomorphism from a commutative semiring to the product of its localizations at all maximal ideals. It is always injective.

Equations

• MaximalSpectrum.toPiLocalization R = algebraMap R (MaximalSpectrum.PiLocalization R)

theorem MaximalSpectrum.toPiLocalization_injective (R : Type u_1) [CommSemiring R] : Function.Injective ⇑(MaximalSpectrum.toPiLocalization R)

theorem MaximalSpectrum.toPiLocalization_apply_apply (R : Type u_1) [CommSemiring R] {r : R} {I : MaximalSpectrum R} : (MaximalSpectrum.toPiLocalization R) r I = (algebraMap R (Localization.AtPrime I.asIdeal)) r

noncomputable def MaximalSpectrum.mapPiLocalization {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Bijective ⇑f) : MaximalSpectrum.PiLocalization R →+* MaximalSpectrum.PiLocalization S

Functoriality of PiLocalization but restricted to bijective ring homs. If R and S are commutative rings, surjectivity would be enough.

Equations

• One or more equations did not get rendered due to their size.

theorem MaximalSpectrum.mapPiLocalization_naturality {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Bijective ⇑f) : (MaximalSpectrum.mapPiLocalization f hf).comp (MaximalSpectrum.toPiLocalization R) = (MaximalSpectrum.toPiLocalization S).comp f

theorem MaximalSpectrum.mapPiLocalization_id {R : Type u_1} [CommSemiring R] : MaximalSpectrum.mapPiLocalization (RingHom.id R) ⋯ = RingHom.id (MaximalSpectrum.PiLocalization R)

theorem MaximalSpectrum.mapPiLocalization_comp {R : Type u_1} {S : Type u_2} (P : Type u_3) [CommSemiring R] [CommSemiring S] [CommSemiring P] (f : R →+* S) (g : S →+* P) (hf : Function.Bijective ⇑f) (hg : Function.Bijective ⇑g) : MaximalSpectrum.mapPiLocalization (g.comp f) ⋯ = (MaximalSpectrum.mapPiLocalization g hg).comp (MaximalSpectrum.mapPiLocalization f hf)

theorem MaximalSpectrum.mapPiLocalization_bijective {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(MaximalSpectrum.mapPiLocalization f hf)

theorem MaximalSpectrum.toPiLocalization_not_surjective_of_infinite {ι : Type u_5} (R : ι → Type u_4) [(i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)] [Infinite ι] : ¬Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))

theorem MaximalSpectrum.finite_of_toPiLocalization_pi_surjective {ι : Type u_5} {R : ι → Type u_4} [(i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)] (h : Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))) : Finite ι

theorem MaximalSpectrum.finite_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R)) : Finite (MaximalSpectrum R)

@[reducible, inline]

abbrev PrimeSpectrum.PiLocalization (R : Type u_1) [CommSemiring R] : Type u_1

The product of localizations at all prime ideals of a commutative semiring.

Equations

• PrimeSpectrum.PiLocalization R = ((p : PrimeSpectrum R) → Localization p.asIdeal.primeCompl)

def PrimeSpectrum.toPiLocalization (R : Type u_1) [CommSemiring R] : R →+* PrimeSpectrum.PiLocalization R

The canonical ring homomorphism from a commutative semiring to the product of its localizations at all prime ideals. It is always injective.

Equations

• PrimeSpectrum.toPiLocalization R = algebraMap R (PrimeSpectrum.PiLocalization R)

theorem PrimeSpectrum.toPiLocalization_injective (R : Type u_1) [CommSemiring R] : Function.Injective ⇑(PrimeSpectrum.toPiLocalization R)

def PrimeSpectrum.piLocalizationToMaximal (R : Type u_1) [CommSemiring R] : PrimeSpectrum.PiLocalization R →+* MaximalSpectrum.PiLocalization R

The projection from the product of localizations at primes to the product of localizations at maximal ideals.

Equations

• PrimeSpectrum.piLocalizationToMaximal R = Pi.ringHom fun (I : MaximalSpectrum R) => Pi.evalRingHom (fun (p : PrimeSpectrum R) => Localization p.asIdeal.primeCompl) I.toPrimeSpectrum

theorem PrimeSpectrum.piLocalizationToMaximal_surjective (R : Type u_1) [CommSemiring R] : Function.Surjective ⇑(PrimeSpectrum.piLocalizationToMaximal R)

def PrimeSpectrum.piLocalizationToMaximalEquiv {R : Type u_1} [CommSemiring R] (h : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) : PrimeSpectrum.PiLocalization R ≃+* MaximalSpectrum.PiLocalization R

If R has Krull dimension ≤ 0, then piLocalizationToIsMaximal R is an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem PrimeSpectrum.piLocalizationToMaximal_bijective {R : Type u_1} [CommSemiring R] (h : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) : Function.Bijective ⇑(PrimeSpectrum.piLocalizationToMaximal R)

theorem PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization {R : Type u_1} [CommSemiring R] : (PrimeSpectrum.piLocalizationToMaximal R).comp (PrimeSpectrum.toPiLocalization R) = MaximalSpectrum.toPiLocalization R

theorem PrimeSpectrum.isMaximal_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R)) (I : PrimeSpectrum R) : I.asIdeal.IsMaximal

noncomputable def PrimeSpectrum.mapPiLocalization {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) : PrimeSpectrum.PiLocalization R →+* PrimeSpectrum.PiLocalization S

A ring homomorphism induces a homomorphism between the products of localizations at primes.

Equations

• One or more equations did not get rendered due to their size.

theorem PrimeSpectrum.mapPiLocalization_naturality {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) : (PrimeSpectrum.mapPiLocalization f).comp (PrimeSpectrum.toPiLocalization R) = (PrimeSpectrum.toPiLocalization S).comp f

theorem PrimeSpectrum.mapPiLocalization_id {R : Type u_1} [CommSemiring R] : PrimeSpectrum.mapPiLocalization (RingHom.id R) = RingHom.id (PrimeSpectrum.PiLocalization R)

theorem PrimeSpectrum.mapPiLocalization_comp {R : Type u_1} {S : Type u_2} (P : Type u_3) [CommSemiring R] [CommSemiring S] [CommSemiring P] (f : R →+* S) (g : S →+* P) : PrimeSpectrum.mapPiLocalization (g.comp f) = (PrimeSpectrum.mapPiLocalization g).comp (PrimeSpectrum.mapPiLocalization f)

theorem PrimeSpectrum.mapPiLocalization_bijective {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(PrimeSpectrum.mapPiLocalization f)

theorem PrimeSpectrum.toPiLocalization_not_surjective_of_infinite {ι : Type u_5} (R : ι → Type u_4) [(i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)] [Infinite ι] : ¬Function.Surjective ⇑(PrimeSpectrum.toPiLocalization ((i : ι) → R i))

theorem PrimeSpectrum.finite_of_toPiLocalization_pi_surjective {ι : Type u_5} {R : ι → Type u_4} [(i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)] (h : Function.Surjective ⇑(PrimeSpectrum.toPiLocalization ((i : ι) → R i))) : Finite ι

theorem PrimeSpectrum.finite_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R)) : Finite (PrimeSpectrum R)