Commit 2024-12-10 08:25 5d2254fa

feat: PrimeSpectrum has DiscreteTopology iff toLocalization is bijective (#19714) Third PR in the series #18891 and #19496 Main results:

• PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective: the prime spectrum of a comm. semiring has discrete Zariski topology iff the map into the product of localizations at primes is surjective (equivalently, bijective).
• mapPiEvalRingHom_bijective: the localization of a product ring $\prod_i R_i$ w.r.t. a "cylindrical" submonoid (of the form $\pi_i^{-1}(S)$, where S is a submonoid of some $R_i$) is canonically isomorphic to the localization of $R_i$ w.r.t. S.
• exists_maximal_nmem_range_sigmaToPi_of_infinite: an infinite product of nontrivial rings has a maximal ideal that is not cylindrical. As a consequence, the map to the product of localizations at maximal ideals cannot be surjective (MaximalSpectrum.toPiLocalization_not_surjective_of_infinite), since the value at the non-cylindrical max ideal is determined by the values at the cylindrical max ideals. As a further consequence, if a ring is isomorphic to the product of its localizations at maximal ideals, the number of maximal ideals must be finite (MaximalSpectrum.finite_of_toPiLocalization_surjective). We rename RingHom.toLocalizationIsMaximal to MaximalSpectrum.toPiLocalization and similarly for associated lemmas. These were introduced in the previous two PRs and are relatively new, so I hope I won't need to add deprecations.