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.lean.

(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.lean). 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

theorem PrimeSpectrum.ext_iff {R : Type u_1} {inst✝ : CommSemiring R} {x y : PrimeSpectrum R} : x = y ↔ x.asIdeal = y.asIdeal

The specialization order

We endow PrimeSpectrum R with a partial order induced from the ideal lattice. This is exactly the specialization order. See the corresponding section at Mathlib/RingTheory/Spectrum/Prime/Topology.lean.

instance PrimeSpectrum.instPartialOrder {R : Type u_1} [CommSemiring R] : PartialOrder (PrimeSpectrum R)

Equations

• PrimeSpectrum.instPartialOrder = PartialOrder.lift PrimeSpectrum.asIdeal ⋯

@[simp]

theorem PrimeSpectrum.asIdeal_le_asIdeal {R : Type u_1} [CommSemiring R] (x y : PrimeSpectrum R) : x.asIdeal ≤ y.asIdeal ↔ x ≤ y

@[simp]

theorem PrimeSpectrum.asIdeal_lt_asIdeal {R : Type u_1} [CommSemiring R] (x y : PrimeSpectrum R) : x.asIdeal < y.asIdeal ↔ x < y

def PrimeSpectrum.equivSubtype (R : Type u_1) [CommSemiring R] : PrimeSpectrum R ≃o { I : Ideal R // I.IsPrime }

The prime spectrum is in bijection with the set of prime ideals.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PrimeSpectrum.equivSubtype_symm_apply_asIdeal (R : Type u_1) [CommSemiring R] (I : { I : Ideal R // I.IsPrime }) : ((RelIso.symm (equivSubtype R)) I).asIdeal = ↑I

@[simp]

theorem PrimeSpectrum.equivSubtype_apply_coe (R : Type u_1) [CommSemiring R] (I : PrimeSpectrum R) : ↑((equivSubtype R) I) = I.asIdeal