Documentation

Mathlib.RingTheory.Spectrum.Maximal.Basic

Maximal spectrum of a commutative (semi)ring #

Basic properties the maximal spectrum of a ring.

source
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.
Instances For
    source
    @[simp]
    theorem MaximalSpectrum.equivSubtype_symm_apply_asIdeal (R : Type u_1) [CommSemiring R] (I : { I : Ideal R // I.IsMaximal }) :
    ((MaximalSpectrum.equivSubtype R).symm I).asIdeal = ↑I
    source
    @[simp]
    theorem MaximalSpectrum.equivSubtype_apply_coe (R : Type u_1) [CommSemiring R] (I : MaximalSpectrum R) :
    ↑((MaximalSpectrum.equivSubtype R) I) = I.asIdeal
    source
    theorem MaximalSpectrum.range_asIdeal (R : Type u_1) [CommSemiring R] :
    Set.range MaximalSpectrum.asIdeal = {J : Ideal R | J.IsMaximal}
    source
    instance MaximalSpectrum.instNonemptyOfNontrivial {R : Type u_1} [CommSemiring R] [Nontrivial R] :
    Nonempty (MaximalSpectrum R)
    source
    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 := ⋯ }
    Instances For
      source
      theorem MaximalSpectrum.toPrimeSpectrum_injective {R : Type u_1} [CommSemiring R] :
      Function.Injective MaximalSpectrum.toPrimeSpectrum