theorem height_principal_le_one {R : Type u_1} [CommRing R] [IsNoetherianRing R] (f : R) (P : Ideal R) [P.IsPrime] (hP : P ∈ (Ideal.span {f}).minimalPrimes) : P.height ≤ 1

Helper: a minimal prime over a principal ideal in a Noetherian ring has height at most one (one half of Krull's principal ideal theorem).

theorem height_le_card_of_minimalPrimes_span {R : Type u_1} [CommRing R] [IsNoetherianRing R] {P : Ideal R} {s : Finset R} (hP : P ∈ (Ideal.span ↑s).minimalPrimes) : P.height ≤ ↑s.card

Generalized Krull height theorem: a minimal prime over a finitely generated ideal has height at most the number of generators.

theorem exists_generators_card_eq_height {R : Type u_1} [CommRing R] [IsNoetherianRing R] (P : Ideal R) [P.IsPrime] : ∃ (s : Finset R), P ∈ (Ideal.span ↑s).minimalPrimes ∧ ↑s.card = P.height

Sharp converse: every prime in a Noetherian ring is a minimal prime over an ideal generated by exactly height P elements.

theorem dim_quotient_nonZeroDivisor_succ_le {R : Type u_1} [CommRing R] {f : R} (hf : f ∈ nonZeroDivisors R) : ringKrullDim (R ⧸ Ideal.span {f}) + 1 ≤ ringKrullDim R

Quotienting by a nonzero-divisor f drops Krull dimension by at least one.

theorem height_le_dim_quotient_principal_succ {R : Type u_1} [CommRing R] [IsNoetherianRing R] {f : R} {P : Ideal R} [P.IsPrime] (hf : f ∈ P) : ↑P.height ≤ ringKrullDim (R ⧸ Ideal.span {f}) + 1

Upper bound on height P in terms of the Krull dimension of R/(f) for f ∈ P.

theorem height_le_dim_quotient_add_encard {R : Type u_1} [CommRing R] [IsNoetherianRing R] {P : Ideal R} [P.IsPrime] (s : Set R) (hs : s ⊆ ↑P) : ↑P.height ≤ ringKrullDim (R ⧸ Ideal.span s) + ↑s.encard

Intersection dimension (Thm 8.1, Lec 8): the height of a prime P containing a set s is bounded by dim(R/(s)) + |s|. Codimension of an irreducible component of X ∩ Y is at most codim X + codim Y.

theorem ringKrullDim_quotient_le_of_le {R : Type u_1} [CommRing R] {I J : Ideal R} (h : I ≤ J) : ringKrullDim (R ⧸ J) ≤ ringKrullDim (R ⧸ I)

Monotonicity: if I ⊆ J then dim(R/J) ≤ dim(R/I).