Hilbert's basis theorem

In mathematics, Hilbert's basis theorem states that every ideal in the ring of multivariate polynomials over a field is finitely generated. This can be translated into algebraic geometry as follows: every algebraic set over a field can be described as the set of common roots of finitely many polynomial equations. The theorem is named for the German mathematician David Hilbert who first proved it in 1888.

Hilbert produced an innovative proof by contradiction using mathematical induction; his method does not give an algorithm to produce the finitely many basis polynomials for a given ideal: it only shows that they must exist. One can determine basis polynomials using the method of Gröbner bases.

Proof

The following more general statement will be proved: if R is a left (respectively right) Noetherian ring then the polynomial ring R[X] is also a left (respectively right) Noetherian ring.

Let I be an ideal in R[X] and assume for a contradiction that I is not finitely generated. Inductively construct a sequence f₁, f₂, ... of elements of I such that f_i+1 has minimal degree in I \ J_i, where J_i is the ideal generated by f₁, ..., f_i. Let a_i be the leading coefficient of f_i and let J be the ideal of R generated by a₁, a₂, ... Since R is Noetherian there exists an integer N such that J is generated by a₁, ..., a_N, so in particular a_N+1 = u₁a₁ + ... + u_Na_N for some u₁, ..., u_N in R. Now consider g = u₁f₁x^n₁ + ... + u_Nf_Nx^n_N where n_i = deg f_N+1 − deg f_i. Because deg g = deg f_N+1 and the leading coefficients of g and f_N+1 agree, the difference f_N+1 − g has degree strictly less than the degree of f_N+1, contradicting the choice of f_N+1. Therefore I is finitely generated, and the proof is complete.

A constructive proof also exists: Given an ideal I of R[X], let L be the set of leading coefficients of the elements of I. Then L is an ideal in R so is finitely generated by a₁,... ,a_n in L, and pick f₁,... ,f_n in I such that the leading coefficient of f_i is a_i. Let d_i be the degree of f_i and let N be the maximum of the d_i. Now for each k = 0, ..., N − 1 let L_k be the set of leading coefficients of elements of I with degree at most k. Then again, L_k is an ideal in R, so is finitely generated by a^k₁,... ,a^k_{m_k} say. As before, let f^k_i in I have leading coefficient a^k_i. Let H be the ideal in R[X] generated by the f_i and the f^k_i. Then surely H is contained in I and assume there is an element f in I not belonging to H, of least degree d, and leading coefficient a. If d is larger than or equal to N then a is in L so, a = r₁a₁ + ... + r_na_n and g = r₁X^d−d₁f₁ + ... + r_nX^d−d_nf_n is of the same degree as f and has the same leading coefficient. Since g is in H, f − g is not, which contradicts the minimality of f. If on the other hand d is strictly smaller than N, then a is in L_d, so a = r₁a^d₁ + ... + r_{m_d}a^d_{m_d}. A similar construction as above gives the same contradiction. Thus, I = H, which is finitely generated, and this finishes the proof.

Mizar System

The Mizar project has completely formalized and automatically checked a proof of Hilbert's basis theorem in the HILBASIS file.

References

Cox, Little, and O'Shea, Ideals, Varieties, and Algorithms, Springer-Verlag, 1997.