Documentation

Mathlib.RingTheory.Spectrum.Maximal.Defs

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 #

source
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
Instances For
    source
    theorem MaximalSpectrum.ext {R : Type u_1} {inst✝ : CommSemiring R} {x y : MaximalSpectrum R} (asIdeal : x.asIdeal = y.asIdeal) :
    x = y
    source
    @[deprecated MaximalSpectrum.isMaximal (since := "2025-01-16")]
    instance MaximalSpectrum.IsMaximal {R : Type u_1} [CommSemiring R] (self : MaximalSpectrum R) :
    self.asIdeal.IsMaximal

    Alias of MaximalSpectrum.isMaximal.