Krull dimension bounds for finitely generated algebras (for Lemma 8.8)

local-ray-geometry.tex (lem:dimension-infinity): "Every component of such a zero set has dimension at least N − F. The change-of-basis group has dimension D, and its simultaneous scalar subgroup stabilizes every representation. An orbit has dimension equal to that of the group minus that of the stabilizer, so each orbit has dimension at most D − 1."

The dimension theory used:

• ringKrullDim_le_of_isIntegral: integral extensions do not raise the Krull dimension (incomparability);
• ringKrullDim_le_of_noether: by Noether normalization, the Krull dimension of a finitely generated algebra is bounded by the number of variables of any injective polynomial subalgebra bound;
• card_le_of_inj_localization: a polynomial algebra embedding in a localization of a polynomial ring in n variables has at most n variables (transcendence degree);
• height_ge_of_chain: a chain of primes bounds the height from below.

theorem MultiplicativeBasisDeformations.ringKrullDim_le_of_isIntegral (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [Algebra.IsIntegral R A] : ringKrullDim A ≤ ringKrullDim R

Incomparability: an integral extension does not raise the Krull dimension.

theorem MultiplicativeBasisDeformations.ringKrullDim_le_of_noether (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] (n : ℕ) (h : ∀ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] A), Function.Injective ⇑g → s ≤ n) : ringKrullDim A ≤ ↑n

Noether normalization bound.

theorem MultiplicativeBasisDeformations.card_le_of_inj_localization (k : Type u_1) [Field k] {σ : Type} [Fintype σ] (δ : MvPolynomial σ k) (hδ : δ ≠ 0) {s : ℕ} (g : MvPolynomial (Fin s) k →ₐ[k] Localization.Away δ) (hg : Function.Injective ⇑g) : s ≤ Fintype.card σ

Transcendence degree bound: a polynomial algebra in s variables embeds in a localization of a polynomial ring in the variables σ only if s ≤ |σ|.

theorem MultiplicativeBasisDeformations.height_ge_of_chain {R : Type u_2} [CommRing R] (n : ℕ) (P : Fin (n + 1) → Ideal R) (hP : ∀ (i : Fin (n + 1)), (P i).IsPrime) (hlt : ∀ (i : Fin n), P i.castSucc < P i.succ) : ↑n ≤ (P (Fin.last n)).height

Heights from chains of primes.