Documentation

Mathlib.RingTheory.Spectrum.Maximal.Basic

Maximal spectrum of a commutative (semi)ring #

Basic properties the maximal spectrum of a ring.

source
🔸 coverage
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.

Instances For
    source
    📐 coverage
    @[simp]
    theorem MaximalSpectrum.equivSubtype_apply_coe (R : Type u_1) [CommSemiring R] (I : MaximalSpectrum R) :
    ↑((equivSubtype R) I) = I.asIdeal
    source
    📐 coverage
    @[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
    source
    📐 coverage
    theorem MaximalSpectrum.range_asIdeal (R : Type u_1) [CommSemiring R] :
    Set.range asIdeal = {J : Ideal R | J.IsMaximal}
    source
    📐 coverage
    instance MaximalSpectrum.instNonemptyOfNontrivial {R : Type u_1} [CommSemiring R] [Nontrivial R] :
    Nonempty (MaximalSpectrum R)
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      theorem MaximalSpectrum.toPrimeSpectrum_injective {R : Type u_1} [CommSemiring R] :
      Function.Injective toPrimeSpectrum