### Abstract

This entry formalizes the connection between Gröbner bases and Macaulay matrices (sometimes also referred to as `generalized Sylvester matrices'). In particular, it contains a method for computing Gröbner bases, which proceeds by first constructing some Macaulay matrix of the initial set of polynomials, then row-reducing this matrix, and finally converting the result back into a set of polynomials. The output is shown to be a Gröbner basis if the Macaulay matrix constructed in the first step is sufficiently large. In order to obtain concrete upper bounds on the size of the matrix (and hence turn the method into an effectively executable algorithm), Dubé's degree bounds on Gröbner bases are utilized; consequently, they are also part of the formalization.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Groebner_Macaulay

- Degree_Section
- Degree_Bound_Utils
- Groebner_Macaulay
- Binomial_Int
- Poly_Fun
- Monomial_Module
- Dube_Prelims
- Hilbert_Function
- Cone_Decomposition
- Dube_Bound
- Groebner_Macaulay_Examples

### Depends on

- Gröbner Bases Theory

## Cite

×

Groebner_Macaulay-AFP

    @article{Groebner_Macaulay-AFP,
      author  = {Alexander Maletzky},
      title   = {Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Groebner_Macaulay.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 17, 2019 : Isabelle2019