Prime spectrum of a commutative (semi)ring as a type

The prime spectrum of a commutative (semi)ring is the type of all prime ideals.

For the Zariski topology, see Mathlib.RingTheory.Spectrum.Prime.Topology.

(It is also naturally endowed with a sheaf of rings, which is constructed in AlgebraicGeometry.StructureSheaf.)

Main definitions

• PrimeSpectrum R: The prime spectrum of a commutative (semi)ring R, i.e., the set of all prime ideals of R.

structure PrimeSpectrum (R : Type u_1) [CommSemiring R] : Type u_1

The prime spectrum of a commutative (semi)ring R is the type of all prime ideals of R.

It is naturally endowed with a topology (the Zariski topology), and a sheaf of commutative rings (see Mathlib.AlgebraicGeometry.StructureSheaf). It is a fundamental building block in algebraic geometry.

• asIdeal : Ideal R
• isPrime : self.asIdeal.IsPrime

theorem PrimeSpectrum.ext {R : Type u_1} {inst✝ : CommSemiring R} {x y : PrimeSpectrum R} (asIdeal : x.asIdeal = y.asIdeal) : x = y

@[deprecated PrimeSpectrum.isPrime (since := "2024-06-22")]

theorem PrimeSpectrum.IsPrime {R : Type u_1} [CommSemiring R] (self : PrimeSpectrum R) : self.asIdeal.IsPrime

Alias of PrimeSpectrum.isPrime.