Noether normalization lemma

This file contains a proof by Nagata of the Noether normalization lemma.

Main Results

Let A be a finitely generated algebra over a field k. Then there exists a natural number s and an injective homomorphism from k[X_0, X_1, ..., X_(s-1)] to A such that A is integral over k[X_0, X_1, ..., X_(s-1)].

Strategy of the proof

Suppose f is a nonzero polynomial in n+1 variables. First, we construct an algebra equivalence T from k[X_0,...,X_n] to itself such that f is mapped to a polynomial in X_0 with invertible leading coefficient. More precisely, T maps X_i to X_i + X_0 ^ r_i when i ≠ 0, and X_0 to X_0. Here we choose r_i to be up ^ i where up is big enough, so that T maps different monomials of f to polynomials with different degrees in X_0. See degreeOf_t_neq_of_neq.

Secondly, we construct the following maps: let I be an ideal containing f and let φ : k[X_0,...X_{n-1}] ≃ₐ[k] k[X_1,...X_n][X] be the natural isomorphism. hom1 : k[X_0,...X_{n-1}] →ₐ[k[X_0,...X_{n-1}]] k[X_1,...X_n][X]/φ(T(I)) eqv1 : k[X_1,...X_n][X]/φ(T(I)) ≃ₐ[k] k[X_0,...,X_n]/T(I) eqv2 : k[X_0,...,X_n]/T(I) ≃ₐ[k] k[X_0,...,X_n]/I hom2 : k[X_0,...X_(n-1)] →ₐ[k] k[X_0,...X_n]/I hom1 is integral because φ(T(I)) contains a monic polynomial. See hom1_isIntegral. hom2 is integral because it's the composition of integral maps. See hom2_isIntegral.

Finally We use induction to prove there is an injective map from k[X_0,...,X_{s-1}] to k[X_0,...,X_(n-1)]/I.The case n=0 is trivial. For n+1, if I = 0 there is nothing to do. Otherwise, hom2 induces a map φ by quotient kernel. We use the inductive hypothesis on k[X_1,...,X_n] and the kernel of hom2 to get s, g. Composing φ and g we get the desired map since both φ and g are injective and integral.

Reference

• https://stacks.math.columbia.edu/tag/00OW

TODO

• In the final theorems, consider setting s equal to the Krull dimension of R.

@[reducible, inline]

noncomputable abbrev NoetherNormalization.T1 {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (c : k) : MvPolynomial (Fin (n + 1)) k →ₐ[k] MvPolynomial (Fin (n + 1)) k

We construct an algebra map T1 f c which maps X_i into X_i + c • X_0 ^ r_i when i ≠ 0 and X_0 to X_0.

Equations

• One or more equations did not get rendered due to their size.

theorem exists_integral_inj_algHom_of_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

There exists some s ≤ n and an integral injective algebra homomorphism from k[X_0,...,X_(s-1)] to k[X_0,...,X_(n-1)]/I if I ≠ ⊤.

theorem exists_integral_inj_algHom_of_fg (k : Type u_2) (R : Type u_3) [Field k] [CommRing R] [Nontrivial R] [a : Algebra k R] [fin : Algebra.FiniteType k R] : ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R), Function.Injective ⇑g ∧ g.IsIntegral

Noether normalization lemma For a finitely generated algebra A over a field k, there exists a natural number s and an injective homomorphism from k[X_0, X_1, ..., X_(s-1)] to A such that A is integral over k[X_0, X_1, ..., X_(s-1)].

Stacks Tag 00OW

theorem exists_finite_inj_algHom_of_fg (k : Type u_2) (R : Type u_3) [Field k] [CommRing R] [Nontrivial R] [a : Algebra k R] [fin : Algebra.FiniteType k R] : ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R), Function.Injective ⇑g ∧ g.Finite

For a finitely generated algebra A over a field k, there exists a natural number s and an injective homomorphism from k[X_0, X_1, ..., X_(s-1)] to A such that A is finite over k[X_0, X_1, ..., X_(s-1)].