Theorems · Definition · algebraic geometry

PrimeSpectrum.toPiLocalizationEquiv

(R : Type u) → [inst : CommSemiring R] → [DiscreteTopology (PrimeSpectrum R)] → R ≃ₐ[R] PrimeSpectrum.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) prime ideals.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringDiscreteTopology