theorem ringKrullDim_quotient_span_succ_le_of_domain {A : Type u_1} [CommRing A] [IsDomain A] (g : A) (hg : g ≠ 0) : ringKrullDim (A ⧸ Ideal.span {g}) + 1 ≤ ringKrullDim A

Cutting by a nonzero element drops the Krull dimension by at least one: dim(A/(g)) + 1 ≤ dim A for a nonzero g in a domain.

theorem ringKrullDim_localization_away_le {A : Type u_1} [CommRing A] (f : A) : ringKrullDim (Localization.Away f) ≤ ringKrullDim A

Localizing away from f can only decrease the Krull dimension: dim A[f⁻¹] ≤ dim A.

theorem height_preserved_by_localization_away {A : Type u_1} [CommRing A] [IsNoetherianRing A] (f : A) (P : Ideal A) [P.IsPrime] (hfP : Disjoint ↑(Submonoid.powers f) ↑P) : (Ideal.map (algebraMap A (Localization.Away f)) P).height = P.height

A prime ideal disjoint from {1, f, f², …} has the same height before and after localizing away from f.

theorem exists_prime_height_eq_dim_disjoint_powers {k : Type u_1} [Field k] {A : Type u_2} [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (f : A) (hf : f ≠ 0) : ∃ (P : Ideal A), P.IsPrime ∧ Disjoint ↑(Submonoid.powers f) ↑P ∧ ↑P.height = ringKrullDim A

For a nonzero element f of a finitely generated domain over k, there exists a prime ideal P of maximal height (= dim A) disjoint from the powers of f.

theorem ringKrullDim_le_localization_away_of_finiteType {k : Type u_1} [Field k] {A : Type u_2} [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (f : A) (hf : f ≠ 0) : ringKrullDim A ≤ ringKrullDim (Localization.Away f)

Reverse inequality for finitely generated k-algebras: localizing away from a nonzero element does not decrease the Krull dimension.

theorem ringKrullDim_localization_away_eq_of_finiteType {k : Type u_1} [Field k] {A : Type u_2} [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (f : A) (hf : f ≠ 0) : ringKrullDim (Localization.Away f) = ringKrullDim A

For a nonzero element of a finitely generated k-algebra domain, localizing away preserves the Krull dimension: dim A[f⁻¹] = dim A.

theorem minimalPrime_ne_bot_of_nonzero {A : Type u_1} [CommRing A] [IsDomain A] (g : A) (hg : g ≠ 0) (P : Ideal A) (hP : P ∈ (Ideal.span {g}).minimalPrimes) : P ≠ ⊥

Any minimal prime of a principal ideal (g) with g ≠ 0 in a domain is nonzero.

theorem height_eq_one_of_minimalPrime_span_domain {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (g : A) (hg : g ≠ 0) (P : Ideal A) [P.IsPrime] (hP : P ∈ (Ideal.span {g}).minimalPrimes) : P.height = 1

Krull's principal-ideal theorem in a Noetherian domain: a minimal prime over a nonzero principal ideal has height exactly one.

theorem one_add_ringKrullDim_quotient_minimalPrime_le {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (g : A) (hg : g ≠ 0) (P : Ideal A) [P.IsPrime] (hP : P ∈ (Ideal.span {g}).minimalPrimes) : 1 + ringKrullDim (A ⧸ P) ≤ ringKrullDim A

The catenary inequality applied to a minimal prime of a nonzero principal ideal: 1 + dim(A/P) ≤ dim A.

theorem ringKrullDim_quotient_minimalPrime_le_quotient_span {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (g : A) (_hg : g ≠ 0) (P : Ideal A) [P.IsPrime] (hP : P ∈ (Ideal.span {g}).minimalPrimes) : ringKrullDim (A ⧸ P) ≤ ringKrullDim (A ⧸ Ideal.span {g})

For a minimal prime P over (g), the dimension of A/P is at most the dimension of A/(g), via the surjective quotient map.

theorem height_add_ringKrullDim_quotient_eq_of_mvPolynomial (k : Type u_1) [Field k] (n : ℕ) (P : Ideal (MvPolynomial (Fin n) k)) [P.IsPrime] : ↑P.height + ringKrullDim (MvPolynomial (Fin n) k ⧸ P) = ringKrullDim (MvPolynomial (Fin n) k)

Catenarity for polynomial rings over a field: for any prime P in k[x₁,…,xₙ], height P + dim(k[x]/P) = n.

theorem withBot_ENat_add_one_eq_coe {d : WithBot ℕ∞} {n : ℕ} (hn : n ≥ 1) (h : 1 + d = ↑n) : d = ↑↑(n - 1)

Numeric helper: if 1 + d = n in WithBot ℕ∞ and n ≥ 1, then d = n - 1.

theorem not_irreducible_mvPolynomial_fin_zero (k : Type u_1) [Field k] (f : MvPolynomial (Fin 0) k) : ¬Irreducible f

No element of k = MvPolynomial (Fin 0) k is irreducible (every nonzero element is a unit).

theorem pos_of_irreducible_mvPolynomial (k : Type u_1) [Field k] (n : ℕ) (f : MvPolynomial (Fin n) k) (hf : Irreducible f) : n ≥ 1

If MvPolynomial (Fin n) k admits an irreducible element, then n ≥ 1.

theorem height_span_irreducible_mvPolynomial (k : Type u_1) [Field k] (n : ℕ) (f : MvPolynomial (Fin n) k) (hf : Irreducible f) : (Ideal.span {f}).height = 1

The ideal (f) cut out by an irreducible polynomial in k[x₁,…,xₙ] has height one.

theorem one_add_ringKrullDim_quotient_minimalPrime_eq_of_mvPolynomial (k : Type u_1) [Field k] (n : ℕ) (g : MvPolynomial (Fin n) k) (hg : g ≠ 0) (P : Ideal (MvPolynomial (Fin n) k)) [P.IsPrime] (hP : P ∈ (Ideal.span {g}).minimalPrimes) : 1 + ringKrullDim (MvPolynomial (Fin n) k ⧸ P) = ringKrullDim (MvPolynomial (Fin n) k)

Catenarity in the polynomial ring: for a minimal prime P of (g) with g ≠ 0, 1 + dim(k[x]/P) = dim k[x].

theorem hypersurface_dim_eq (k : Type u_1) [Field k] (n : ℕ) (f : MvPolynomial (Fin n) k) (hf : Irreducible f) : ringKrullDim (MvPolynomial (Fin n) k ⧸ Ideal.span {f}) = ↑(n - 1)

Dimension of an irreducible hypersurface in affine n-space: dim(k[x₁,…,xₙ] / (f)) = n - 1 for f irreducible.