Krull dimension of polynomial ring

This file proves properties of the Krull dimension of the polynomial ring over a commutative ring

Main results

• Polynomial.ringKrullDim_le: the Krull dimension of the polynomial ring over a commutative ring R is less than 2 * (ringKrullDim R) + 1.

For noetherian rings:

• Polynomial.ringKrullDim_of_isNoetherianRing: the Krull dimension of R[X] is dim R + 1.
• MvPolynomial.ringKrullDim_of_isNoetherianRing: the Krull dimension of R[X₁, ..., Xₙ] is dim R + n.

theorem Polynomial.ringKrullDim_le {R : Type u_1} [CommRing R] : ringKrullDim (Polynomial R) ≤ 2 * ringKrullDim R + 1

theorem Polynomial.height_map_C {R : Type u_1} [CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsMaximal] : (Ideal.map C p).height = p.height

Let p be a maximal ideal of R. Then the height of p[X] equals the height of p.

theorem Polynomial.height_eq_height_add_one {R : Type u_1} [CommRing R] [IsNoetherianRing R] (p : Ideal R) (P : Ideal (Polynomial R)) [P.IsMaximal] [P.LiesOver p] : P.height = p.height + 1

Let p be a prime ideal of R. If P is a maximal ideal of R[X] lying over p, ht(P) = ht(p) + 1.

@[simp]

theorem Polynomial.ringKrullDim_of_isNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] : ringKrullDim (Polynomial R) = ringKrullDim R + 1

If R is Noetherian, dim R[X] = dim R + 1.

@[simp]

theorem MvPolynomial.ringKrullDim_of_isNoetherianRing_of_finite {R : Type u_1} [CommRing R] [IsNoetherianRing R] {ι : Type u_2} [Finite ι] : ringKrullDim (MvPolynomial ι R) = ringKrullDim R + ↑(Nat.card ι)

If R is Noetherian, dim R[X₁, ..., Xₙ] = dim R + n.

theorem MvPolynomial.ringKrullDim_of_isNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] {ι : Type u_2} : ringKrullDim (MvPolynomial ι R) = ringKrullDim R + ↑(ENat.card ι)

If R is Noetherian, dim R[Xₛ] = dim R + card(Xₛ).