Documentation

Mathlib.RingTheory.KrullDimension.Basic

Krull dimensions of (commutative) rings #

Given a commutative ring, its ring-theoretic Krull dimension is the order-theoretic Krull dimension of its prime spectrum. Unfolding this definition, it is the length of the longest sequence(s) of prime ideals ordered by strict inclusion.

noncomputable def ringKrullDim (R : Type u_1) [CommSemiring R] :

The ring-theoretic Krull dimension is the Krull dimension of its spectrum ordered by inclusion.

Equations
Instances For
    @[reducible, inline]
    abbrev Ring.KrullDimLE (n : ) (R : Type u_1) [CommSemiring R] :

    Type class for rings with krull dimension at most n.

    Equations
    Instances For

      If f : R →+* S is surjective, then ringKrullDim S ≤ ringKrullDim R.

      If I is an ideal of R, then ringKrullDim (R ⧸ I) ≤ ringKrullDim R.

      If R and S are isomorphic, then ringKrullDim R = ringKrullDim S.

      Alias of ringKrullDim_eq_of_ringEquiv.


      If R and S are isomorphic, then ringKrullDim R = ringKrullDim S.

      @[reducible, inline]

      A ring has finite Krull dimension if its PrimeSpectrum is finite-dimensional (and non-empty).

      Equations
      Instances For
        theorem Ring.krullDimLE_zero_iff {R : Type u_1} [CommSemiring R] :
        KrullDimLE 0 R ∀ (I : Ideal R), I.IsPrimeI.IsMaximal
        theorem Ring.KrullDimLE.mk₀ {R : Type u_1} [CommSemiring R] (H : ∀ (I : Ideal R), I.IsPrimeI.IsMaximal) :
        theorem Ideal.IsPrime.isMaximal' {R : Type u_1} [CommSemiring R] [Ring.KrullDimLE 0 R] {I : Ideal R} (hI : I.IsPrime) :

        Also see Ideal.IsPrime.isMaximal for the analogous statement for Dedekind domains.

        theorem Ring.KrullDimLE.mk₁ {R : Type u_1} [CommSemiring R] (H : ∀ (I : Ideal R), I.IsPrimeI minimalPrimes R I.IsMaximal) :
        theorem Ring.KrullDimLE.mk₁' {R : Type u_1} [CommSemiring R] (H : ∀ (I : Ideal R), I I.IsPrimeI.IsMaximal) :

        Alternative constructor for Ring.KrullDimLE 1, convenient for domains.