theorem noether_normalization_integral (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : ∃ (d : ℕ) (g : MvPolynomial (Fin d) k →ₐ[k] A), Function.Injective ⇑g ∧ g.IsIntegral

Noether normalization (integral form): a finitely generated k-algebra A contains a polynomial subring k[x_1,...,x_d] over which A is integral (Lemma 1, Lecture 2).

theorem noether_normalization_finite (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : ∃ (d : ℕ) (g : MvPolynomial (Fin d) k →ₐ[k] A), Function.Injective ⇑g ∧ g.Finite

Noether normalization (module-finite form): A is a finitely generated module over some polynomial subring k[x_1,...,x_d] (Theorem 3.2, Lecture 3).

theorem noether_normalization_spec_surjective (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : ∃ (d : ℕ) (g : MvPolynomial (Fin d) k →ₐ[k] A), Function.Injective ⇑g ∧ g.Finite ∧ Function.Surjective (PrimeSpectrum.comap g.toRingHom)

Geometric form of Noether normalization: the induced map on spectra Spec A → Spec k[x_1,...,x_d] is surjective.

theorem noether_normalization_implies_zariski_lemma (k : Type u_1) (A : Type u_2) [Field k] [Field A] [Algebra k A] [Algebra.FiniteType k A] : Algebra.IsAlgebraic k A

Zariski's lemma via Noether normalization: any finitely generated k-algebra that is a field must be algebraic over k.

theorem zariski_lemma_module_finite (k : Type u_1) (A : Type u_2) [Field k] [Field A] [Algebra k A] [Algebra.FiniteType k A] : Module.Finite k A

Strengthened Zariski lemma: a finitely generated k-algebra which is a field is in fact finite-dimensional as a k-vector space.

theorem noether_normalization_dimension (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : ∃ (d : ℕ) (g : MvPolynomial (Fin d) k →ₐ[k] A), Function.Injective ⇑g ∧ g.Finite ∧ ringKrullDim A = ↑d

Noether normalization computes the Krull dimension: the integer d such that A is module-finite over k[x_1,...,x_d] equals dim A.

theorem noether_normalization_dim_is_nat (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : ∃ (d : ℕ), ringKrullDim A = ↑d

The Krull dimension of any finitely generated algebra over a field is a natural number (finite and non-negative).

theorem dim_preserved_by_finite_injective {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] (hinj : Function.Injective ⇑(algebraMap B A)) : ringKrullDim A = ringKrullDim B

A finite injective ring extension preserves Krull dimension: going-up and incomparability give matching prime chains in A and B.

theorem noether_normalization_quotient {k : Type u_1} [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (hI : I ≠ ⊤) : ∃ s ≤ n, ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ I), Function.Injective ⇑g ∧ g.IsIntegral

Noether normalization for quotients of polynomial rings: for a proper ideal I in k[x_1,...,x_n], the quotient is integral over some k[y_1,...,y_s] with s ≤ n.

theorem algebraic_variety_finite_dimension (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.Scheme.IsAlgebraicVariety k X] : ∃ (d : ℕ), topologicalKrullDim ↥X = ↑d

An algebraic variety over a field has finite (natural number) Krull dimension as a topological space.