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
    Instances For
      source
      @[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
      @[simp]
      theorem MaximalSpectrum.equivSubtype_apply_coe (R : Type u_1) [CommSemiring R] (I : MaximalSpectrum R) :
      ↑((equivSubtype R) I) = I.asIdeal
      source
      theorem MaximalSpectrum.range_asIdeal (R : Type u_1) [CommSemiring R] :
      Set.range 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
        Instances For
          source
          theorem MaximalSpectrum.toPrimeSpectrum_injective {R : Type u_1} [CommSemiring R] :
          Function.Injective toPrimeSpectrum