Krull dimension and non-zero-divisors

Main results

• ringKrullDim_quotient_succ_le_of_nonZeroDivisor: If r is not a zero divisor, then dim R/r + 1 ≤ dim R.
• ringKrullDim_succ_le_ringKrullDim_polynomial: dim R + 1 ≤ dim R[X].
• ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial: dim R + #σ ≤ dim R[σ].

theorem ringKrullDim_quotient {R : Type u_1} [CommRing R] (I : Ideal R) : ringKrullDim (R ⧸ I) = Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I)

theorem ringKrullDim_quotient_succ_le_of_nonZeroDivisor {R : Type u_1} [CommRing R] {r : R} (hr : r ∈ nonZeroDivisors R) : ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R

theorem ringKrullDim_succ_le_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) {r : R} (hr : r ∈ nonZeroDivisors R) (hr' : f r = 0) : ringKrullDim S + 1 ≤ ringKrullDim R

If R →+* S is surjective whose kernel contains a nonzero divisor, then dim S + 1 ≤ dim R.

theorem ringKrullDim_succ_le_ringKrullDim_polynomial {R : Type u_1} [CommRing R] : ringKrullDim R + 1 ≤ ringKrullDim (Polynomial R)

@[simp]

theorem ringKrullDim_mvPolynomial_of_isEmpty {R : Type u_1} [CommRing R] (σ : Type u_3) [IsEmpty σ] : ringKrullDim (MvPolynomial σ R) = ringKrullDim R

theorem ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial {R : Type u_1} [CommRing R] (σ : Type u_3) [Finite σ] : ringKrullDim R + ↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

theorem ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial {R : Type u_1} [CommRing R] (σ : Type u_3) : ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

@[simp]

theorem ringKrullDim_mvPolynomial_of_infinite {R : Type u_1} [CommRing R] [Nontrivial R] {σ : Type u_3} [Infinite σ] : ringKrullDim (MvPolynomial σ R) = ⊤

If R is non-trivial, a polynomial ring in an infinite number of variables has infinite height, i.e. dim R[X₁, ...] = ∞.

theorem ringKrullDim_succ_le_ringKrullDim_powerseries {R : Type u_1} [CommRing R] : ringKrullDim R + 1 ≤ ringKrullDim (PowerSeries R)