Maximal spectrum of a commutative (semi)ring

Basic properties the maximal spectrum of a ring.

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)