Commit 2024-11-25 16:30 551481f4

feat: ring with discrete PrimeSpectrum (#18891) Prove two characterizations of commutative semirings R whose prime spectra have discrete topology:

• R has finitely many prime ideals, and every prime ideal is maximal;
• R has finitely many maximal ideals, the intersection of which (= Jacobson radical) is contained in (and therefore equal to) the nilradical. From the first characterization it is easy to show the spectrum of an Artinian ring has discrete topology, but Artinian doesn't currently import PrimeSpectrum. Also show that if R is a commutative ring and Spec R has discrete topology, then the canonical RingHom from R to the product of localizations at maximal ideals (which is always injective) is an isomorphism. This is not a characterization, because it is satisfied by every local ring. (But it's a characterization if we replace "maximal" by "prime".) For this purpose we prove that, if a basic open D(f) in Spec R is a singleton {p}, then localization away from f is the same as localization at p. A key fact used is that if an ideal in a commutative semiring is disjoint from a submonoid, then there exists a maximal such ideal containing the ideal, and any maximal such ideal is prime. Also upgrade exists_idempotent_basicOpen_eq_of_isClopen to existsUnique.