English
Under the assumption of discreteness of the Zariski topology, R is canonically isomorphic to MaximalSpectrum.PiLocalization(R).
Русский
При дискретной топологии Zariski кольцо R канонически изоморфно MaximalSpectrum.PiLocalization(R).
LaTeX
$$$$ R \cong+* \operatorname{MaximalSpectrum.PiLocalization}(R). $$$$
Lean4
/-- If the prime spectrum of a commutative semiring R has discrete Zariski topology, then R is
canonically isomorphic to the product of its localizations at the (finitely many) maximal ideals. -/
@[stacks 00JA "See also `PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical`."]
def _root_.MaximalSpectrum.toPiLocalizationEquiv : R ≃+* MaximalSpectrum.PiLocalization R :=
.ofBijective _
⟨MaximalSpectrum.toPiLocalization_injective R, maximalSpectrumToPiLocalization_surjective_of_discreteTopology R⟩
