Maximal spectrum of a commutative (semi)ring

The maximal spectrum of a commutative (semi)ring is the type of all maximal ideals. It is naturally a subset of the prime spectrum endowed with the subspace topology.

Main definitions

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

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

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

• asIdeal : Ideal R
• isMaximal : self.asIdeal.IsMaximal

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

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

@[instance_reducible]

instance instCoeMaximalSpectrumIdeal (R : Type u_1) [CommSemiring R] : Coe (MaximalSpectrum R) (Ideal R)

Equations

• instCoeMaximalSpectrumIdeal R = { coe := fun (P : MaximalSpectrum R) => P.asIdeal }