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

@[deprecated MaximalSpectrum.isMaximal (since := "2025-01-16")]

theorem MaximalSpectrum.IsMaximal {R : Type u_1} [CommSemiring R] (self : MaximalSpectrum R) : self.asIdeal.IsMaximal

Alias of MaximalSpectrum.isMaximal.