![](http://image.absoluteastronomy.com/images//topicimages/noimage.gif)
Hilbert's basis theorem
Encyclopedia
In mathematics
, specifically commutative algebra
, Hilbert's basis theorem states that every ideal
in the ring of multivariate polynomials
over a Noetherian ring
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. proved the theorem (for the special case of polynomial rings over a field) in the course of his proof of finite generation of rings of invariants.
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
.
Theorem. If
is a left- (respectively right-) Noetherian ring
, then the polynomial ring
is also a left- (respectively right-) Noetherian ring.
It suffices to consider just the "Left" case.
Proof (Theorem)
Suppose per contra that
were a non-finitely generated left-ideal. Then it would be that by recursion (using the countable axiom of choice) that a sequence
of polynomials could be found so that, letting
of minimal degree. It is clear that
is a non-decreasing sequence of naturals. Now consider the left-ideal
over
where the
are the leading coefficients of the
. Since
is left-Noetherian, we have that
must be finitely generated; and since the
comprise an
-basis, it follows that for a finite amount of them, say
will suffice. So for example,
some
Now consider
whose leading term is equal to that of
moreover
so
of degree
contradicting minimality.
A constructive proof
(not invoking the axiom of choice) also exists.
Proof (Theorem):
Let
be a left-ideal. Let
be the set of leading coefficients of members of
This is obviously a left-ideal over
and so is finitely generated by the leading coefficients of finitely many members of
say
Let
Let
be the set of leading coefficients of members of
whose degree is
As before, the
are left-ideals over
and so are finitely generated by the leading coefficients of finitely many members of
say
with degrees
Now let
be the left-ideal generated by
We have
and claim also ![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-43.gif)
Suppose per contra this were not so. Then let
be of minimal degree, and denote its leading coefficient by ![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-45.gif)
Case 1:
Regardless of this condition, we have
so is a left-linear combination
of the coefficients of the
Consider
which has the same leading term as
moreover
so
of degree
contradicting minimality.
Case 2:
Then
so is a left-linear combination
of the leading coefficients of the
Considering
we yield a similar contradiction as in Case 1.
Thus our claim holds, and
which is finitely generated.
Note that the only reason we had to split into two cases was to ensure that the powers of
multiplying the factors, were non-negative in the constructions.
be a Nötherian commutative ring. Hilbert's basis theorem has some immediate corollaries. First, by induction we see that
will also be Nötherian. Second, since any affine variety over
(i.e. a locus-set of a collection of polynomials) may be written as the locus of an ideal
and further as the locus of its generators, it follows that every affine variety is the locus of finitely many polynomials — i.e. the intersection of finitely many hypersurfaces
. Finally, if
were a finitely-generated
-algebra, then we know that
(i.e. mod-ing out by relations), where
a set of polynomials. We can assume that
is an ideal and thus is finitely generated. So
would be a free
-algebra (on
generators) generated by finitely many relations
.
has completely formalized and automatically checked a proof of Hilbert's basis theorem in the HILBASIS file.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, specifically commutative algebra
Commutative algebra
Commutative algebra is the branch of abstract algebra that studies commutative rings, their ideals, and modules over such rings. Both algebraic geometry and algebraic number theory build on commutative algebra...
, Hilbert's basis theorem states that every ideal
Ideal (ring theory)
In ring theory, a branch of abstract algebra, an ideal is a special subset of a ring. The ideal concept allows the generalization in an appropriate way of some important properties of integers like "even number" or "multiple of 3"....
in the ring of multivariate polynomials
Polynomial ring
In mathematics, especially in the field of abstract algebra, a polynomial ring is a ring formed from the set of polynomials in one or more variables with coefficients in another ring. Polynomial rings have influenced much of mathematics, from the Hilbert basis theorem, to the construction of...
over a Noetherian ring
Noetherian ring
In mathematics, more specifically in the area of modern algebra known as ring theory, a Noetherian ring, named after Emmy Noether, is a ring in which every non-empty set of ideals has a maximal element...
is finitely generated. This can be translated into algebraic geometry
Algebraic geometry
Algebraic geometry is a branch of mathematics which combines techniques of abstract algebra, especially commutative algebra, with the language and the problems of geometry. It occupies a central place in modern mathematics and has multiple conceptual connections with such diverse fields as complex...
as follows: every algebraic set
Algebraic set
In mathematics, an algebraic set over an algebraically closed field K is the set of solutions in Kn of a set of simultaneous equationsand so on up to...
over a field can be described as the set of common roots of finitely many polynomial equations. proved the theorem (for the special case of polynomial rings over a field) in the course of his proof of finite generation of rings of invariants.
Hilbert produced an innovative proof by contradiction using mathematical induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
; his method does not give an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
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
Gröbner basis
In computer algebra, computational algebraic geometry, and computational commutative algebra, a Gröbner basis is a particular kind of generating subset of an ideal I in a polynomial ring R...
.
Proof
The following more general statement will be proved.Theorem. If
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-1.gif)
Noetherian ring
In mathematics, more specifically in the area of modern algebra known as ring theory, a Noetherian ring, named after Emmy Noether, is a ring in which every non-empty set of ideals has a maximal element...
, then the polynomial ring
Polynomial ring
In mathematics, especially in the field of abstract algebra, a polynomial ring is a ring formed from the set of polynomials in one or more variables with coefficients in another ring. Polynomial rings have influenced much of mathematics, from the Hilbert basis theorem, to the construction of...
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-2.gif)
It suffices to consider just the "Left" case.
Proof (Theorem)
Suppose per contra that
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-3.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-4.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-5.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-6.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-7.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-8.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-9.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-10.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-11.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-12.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-13.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-14.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-15.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-16.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-17.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-18.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-19.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-20.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-21.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-22.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-23.gif)
A constructive proof
Constructive proof
In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object...
(not invoking the axiom of choice) also exists.
Proof (Theorem):
Let
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-25.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-26.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-27.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-28.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-29.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-30.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-31.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-32.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-33.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-34.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-35.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-36.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-37.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-38.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-39.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-40.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-41.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-42.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-43.gif)
Suppose per contra this were not so. Then let
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-44.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-45.gif)
Case 1:
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-46.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-47.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-48.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-49.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-50.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-51.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-52.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-53.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-54.gif)
Case 2:
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-55.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-56.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-57.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-58.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-59.gif)
Thus our claim holds, and
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-60.gif)
Note that the only reason we had to split into two cases was to ensure that the powers of
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-62.gif)
Applications
Let![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-63.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-64.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-65.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-66.gif)
Hypersurface
In geometry, a hypersurface is a generalization of the concept of hyperplane. Suppose an enveloping manifold M has n dimensions; then any submanifold of M of n − 1 dimensions is a hypersurface...
. Finally, if
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-67.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-68.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-69.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-70.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-71.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-72.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-73.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-74.gif)
![](http://image.absoluteastronomy.com/images/formulas/6/5/1656155-75.gif)
Mizar System
The Mizar projectMizar system
The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...
has completely formalized and automatically checked a proof of Hilbert's basis theorem in the HILBASIS file.