Maximal spectrum of a commutative (semi)ring

Basic properties the maximal spectrum of a ring.

def MaximalSpectrum.equivSubtype (R : Type u_1) [CommSemiring R] : MaximalSpectrum R ≃ { I : Ideal R // I.IsMaximal }

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 MaximalSpectrum.equivSubtype_symm_apply_asIdeal (R : Type u_1) [CommSemiring R] (I : { I : Ideal R // I.IsMaximal }) : ((equivSubtype R).symm I).asIdeal = ↑I

@[simp]

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

theorem MaximalSpectrum.range_asIdeal (R : Type u_1) [CommSemiring R] : Set.range asIdeal = {J : Ideal R | J.IsMaximal}

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

theorem MaximalSpectrum.isCoprime_of_ne {R : Type u_1} [CommSemiring R] {I J : MaximalSpectrum R} (h : I ≠ J) : IsCoprime I.asIdeal J.asIdeal