theorem ringKrullDim_mvPolynomial_field (k : Type u_1) [Field k] (n : ℕ) : ringKrullDim (MvPolynomial (Fin n) k) = ↑n

Theorem 5.1 (Lec 5): the Krull dimension of affine n-space over a field equals n, i.e. dim k[X₁,…,Xₙ] = n.

theorem dim_eq_of_ringEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : ringKrullDim R = ringKrullDim S

Krull dimension is invariant under ring isomorphism.

theorem PrimeSpectrum.zeroLocus_prime_eq_Ici {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] : zeroLocus ↑p = Set.Ici { asIdeal := p, isPrime := ⋯ }

The vanishing locus V(p) of a prime ideal p equals the upward closure {q ∈ Spec R : p ⊆ q} in the specialization order.

theorem ringKrullDim_quotient_prime_eq_coheight {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] : ringKrullDim (R ⧸ p) = ↑(Order.coheight { asIdeal := p, isPrime := ⋯ })

For a prime ideal p ⊂ R, dim (R/p) equals the coheight of p in Spec R, since Spec(R/p) is order-isomorphic to V(p) = Ici p.

theorem height_add_ringKrullDim_quotient_le {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] [Nontrivial R] : ↑p.height + ringKrullDim (R ⧸ p) ≤ ringKrullDim R

Height/coheight inequality: for any prime p, height(p) + dim(R/p) ≤ dim(R).