Maximal spectrum of a commutative (semi)ring

Localization results.

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.

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.

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

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

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.

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

theorem MaximalSpectrum.mapPiLocalization_id {R : Type u_1} [CommSemiring R] : mapPiLocalization (RingHom.id R) ⋯ = RingHom.id (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) : mapPiLocalization (g.comp f) ⋯ = (mapPiLocalization g hg).comp (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 ⇑(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 ⇑(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 ⇑(toPiLocalization ((i : ι) → R i))) : Finite ι

theorem MaximalSpectrum.finite_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(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.

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.

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

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.

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

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.

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

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

theorem PrimeSpectrum.isMaximal_of_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] (surj : Function.Surjective ⇑(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) : PiLocalization R →+* PiLocalization S

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

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

theorem PrimeSpectrum.mapPiLocalization_id {R : Type u_1} [CommSemiring R] : mapPiLocalization (RingHom.id R) = RingHom.id (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) : mapPiLocalization (g.comp f) = (mapPiLocalization g).comp (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 ⇑(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 ⇑(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 ⇑(toPiLocalization ((i : ι) → R i))) : Finite ι

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