Theorems · Definition · algebraic geometry

MaximalSpectrum.toPiLocalizationEquiv

(R : Type u) → [inst : CommSemiring R] → [DiscreteTopology (PrimeSpectrum R)] → R ≃ₐ[R] MaximalSpectrum.PiLocalization R

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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

2 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringDiscreteTopology