Email Gateway (Feb 12 2025 at 08:34): Email Gateway (Feb 12 2025 at 08:34):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce a new AFP entry:
A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series
by Benjamin Puyobro, Benoît Ballenghien and Burkhart Wolff
Abstract:
The Hilbert Basis Theorem is enlisted in the extension of Wiedijk's catalogue
"Formalizing 100 Theorems", a well-known collection of challenge problems for
the formalization of mathematics.
In this paper, we present a formal proof of several versions of this theorem in
Isabelle/HOL. Hilbert's basis theorem asserts that every ideal of a polynomial
ring over a commutative ring has a finite generating family (a finite basis in
Hilbert's terminology). A prominent alternative formulation is: every polynomial
ring over a Noetherian ring is also Noetherian.
In more detail, the statement and our generalization can be presented as follows:
Hilbert's Basis Theorem. Let R[X] denote the ring of polynomials in the
indeterminate X over the commutative ring R. Then R[X] is Noetherian if and
only if R is.
Corollary. R[X_1, ..., X_n] is Noetherian if and only if R is.
Extension. If R is a Noetherian ring, then R[[X]] is a Noetherian ring,
where R[[X]] denotes the formal power series over the ring R.
We also provide isomorphisms between the three types of polynomial rings defined
in HOL-Algebra. Together with the fact that the Noetherian property is preserved
by isomorphism, we get Hilbert's Basis Theorem for all three models. We believe
that this technique has a wider potential of applications in the AFP library.
For further details, have a look at:
https://www.isa-afp.org/entries/Hilbert_Basis.html
Enjoy,
René
Last updated: Mar 09 2025 at 12:28 UTC