Maximal spectrum of a commutative (semi)ring

Basic properties the maximal spectrum of a ring.

instance MaximalSpectrum.instNonemptyOfNontrivial {R : Type u_1} [CommSemiring R] [Nontrivial R] : Nonempty (MaximalSpectrum R)

def MaximalSpectrum.toPrimeSpectrum {R : Type u_1} [CommSemiring R] (x : MaximalSpectrum R) : PrimeSpectrum R

The natural inclusion from the maximal spectrum to the prime spectrum.

Equations

• x.toPrimeSpectrum = { asIdeal := x.asIdeal, isPrime := ⋯ }

theorem MaximalSpectrum.toPrimeSpectrum_injective {R : Type u_1} [CommSemiring R] : Function.Injective toPrimeSpectrum