# Maximal spectrum of a commutative (semi)ring #

Localization results.

source
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.

source
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.

source
@[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)

Instances For

source
def MaximalSpectrum.toPiLocalization (R : Type u_1) [CommSemiring R] :
R →+* 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)

Instances For

source
theorem MaximalSpectrum.toPiLocalization_injective (R : Type u_1) [CommSemiring R] :
Function.Injective ⇑(toPiLocalization R)
source
theorem MaximalSpectrum.toPiLocalization_apply_apply (R : Type u_1) [CommSemiring R] {r : R} {I : MaximalSpectrum R} :
(toPiLocalization R) r I = (algebraMap R (Localization.AtPrime I.asIdeal)) r
source
noncomputable def MaximalSpectrum.mapPiLocalization {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Bijective ⇑f) :
PiLocalization R →+* 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.

Instances For

source
theorem MaximalSpectrum.mapPiLocalization_naturality {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Bijective ⇑f) :
(mapPiLocalization f hf).comp (toPiLocalization R) = (toPiLocalization S).comp f
source
theorem MaximalSpectrum.mapPiLocalization_id {R : Type u_1} [CommSemiring R] :
mapPiLocalization (RingHom.id R) ⋯ = RingHom.id (PiLocalization R)
source
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) :
mapPiLocalization (g.comp f) ⋯ = (mapPiLocalization g hg).comp (mapPiLocalization f hf)
source
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 ⇑(mapPiLocalization f hf)
source
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 ⇑(toPiLocalization ((i : ι) → R i))
source
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 ⇑(toPiLocalization ((i : ι) → R i))) :
Finite ι
source
theorem MaximalSpectrum.finite_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(toPiLocalization R)) :
Finite (MaximalSpectrum R)
source
@[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)

Instances For

source
def PrimeSpectrum.toPiLocalization (R : Type u_1) [CommSemiring R] :
R →+* 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)

Instances For

source
theorem PrimeSpectrum.toPiLocalization_injective (R : Type u_1) [CommSemiring R] :
Function.Injective ⇑(toPiLocalization R)
source
def PrimeSpectrum.piLocalizationToMaximal (R : Type u_1) [CommSemiring R] :
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

Instances For

source
theorem PrimeSpectrum.piLocalizationToMaximal_surjective (R : Type u_1) [CommSemiring R] :
Function.Surjective ⇑(piLocalizationToMaximal R)
source
def PrimeSpectrum.piLocalizationToMaximalEquiv {R : Type u_1} [CommSemiring R] (h : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) :
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.

Instances For

source
theorem PrimeSpectrum.piLocalizationToMaximal_bijective {R : Type u_1} [CommSemiring R] (h : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) :
Function.Bijective ⇑(piLocalizationToMaximal R)
source
theorem PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization {R : Type u_1} [CommSemiring R] :
(piLocalizationToMaximal R).comp (toPiLocalization R) = MaximalSpectrum.toPiLocalization R
source
theorem PrimeSpectrum.isMaximal_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(toPiLocalization R)) (I : PrimeSpectrum R) :
I.asIdeal.IsMaximal
source
noncomputable def PrimeSpectrum.mapPiLocalization {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) :
PiLocalization R →+* 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.

Instances For

source
theorem PrimeSpectrum.mapPiLocalization_naturality {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) :
(mapPiLocalization f).comp (toPiLocalization R) = (toPiLocalization S).comp f
source
theorem PrimeSpectrum.mapPiLocalization_id {R : Type u_1} [CommSemiring R] :
mapPiLocalization (RingHom.id R) = RingHom.id (PiLocalization R)
source
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) :
mapPiLocalization (g.comp f) = (mapPiLocalization g).comp (mapPiLocalization f)
source
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 ⇑(mapPiLocalization f)
source
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 ⇑(toPiLocalization ((i : ι) → R i))
source
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 ⇑(toPiLocalization ((i : ι) → R i))) :
Finite ι
source
theorem PrimeSpectrum.finite_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(toPiLocalization R)) :
Finite (PrimeSpectrum R)