# Gröbner Basis

This page has been identified as a candidate for refactoring of advanced complexity.Until this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

This article needs to be linked to other articles.In particular: including CategoriesYou can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{MissingLinks}}` from the code. |

It has been suggested that this page be renamed.In particular: Buchberger's Algorithm? We need another page to define a "Gröbner base".To discuss this page in more detail, feel free to use the talk page. |

## Theorem

Let $F$ be a finite set of polynomials.

This article, or a section of it, needs explaining.In particular: Explain what the underlying field of the polynomials is. Real numbers, abstract rings, general fields? Link to the appropriate definition for the case.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

Let $\map {\operatorname {SP} } {f_1, f_2}$ be the $S$-polynomial of $f_1$ and $f_2$.

Let $g$ be a polynomial.

Let $\map {\operatorname {RF} } g$ be the reduced form of $g$.

Then $F$ is a Gröbner basis if and only if:

- $\forall f_1, f_2 \in \map F {\map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = 0}$

This article, or a section of it, needs explaining.In particular: The meaning of the above needs to be made clear. Presumably it should be interpreted something like: $\forall f_1, f_2 \in F: \map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = 0$. But further to this: $RF$ as defined takes a single argument, a polynomial (still to be defined upon what domain). As this statement stands, $RF$ seems to take two parameters: $F$ and $\operatorname {SP}$. Clarification is needed.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

## Proof

### Necessary Condition

Let $F$ be a Gröbner basis.

Let $f_1, f_2 \in F$.

Then:

- $\map {\operatorname {SP} } {f_1, f_2} \in \map {\operatorname {Ideal} } F$

That is:

- $\map {\operatorname {SP} } {f_1, f_2} \equiv_F 0$

This article, or a section of it, needs explaining.In particular: Link to a result explaining the above.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

By the relation between reduction and congruence this implies that:

- $\map {\operatorname {SP} } {f_1, f_2} \leftrightarrow_F^* 0$

This article, or a section of it, needs explaining.In particular: Define via links to the appropriate pages the meaning of the above.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

Hence:

- $\map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = \map {\operatorname {RF} } {F, 0} = 0$

because $F$ is a Gröbner basis (and because of the equivalence between the Church-Rosser property and the normal form Church-Rosser property).

This article, or a section of it, needs explaining.In particular: Establish the above equivalence and the conclusion drawn from it in a separate page.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

$\Box$

### Sufficient Condition

Let:

- $\forall f_1, f_2 \in \map F {\map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = 0}$

By the generalized Newman lemma and:

- $\gets_F \mathop \subseteq \succ$

it suffices to prove local connectibility.

That is, it suffices to prove that under the assumption:

- $g_1 \to_F h \gets_F g_2$

we have:

- $g_1 \stackrel {\prec h} {\longleftrightarrow^*_F} g_2$

This article, or a section of it, needs explaining.In particular: All the above notation needs to be explained.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

Let $\map {\operatorname {LPP} } f$ be the leading power product of $f$.

Then by the assumption, there exist $f_1, f_2 \in F$ and $t_1, t_2 \in \map S h$ with:

- $\map {\operatorname {LPP} } {f_1} \mathop | t_1$

and:

- $\map {\operatorname {LPP} } {f_2} \mathop | t_2$

such that:

- $h \rightarrow_{f_1, t_1} g_1$

and:

- $h \rightarrow_{f_2, t_2} g_2$

Now we have three cases.

*Case $t_1 \succ t_2$*:

In this case:

\(\ds g_1\) | \(=\) | \(\ds \map H {h, t_1} + 0 \cdot t_1 + \map B {h, t_1, t_2} + \map C {h, t_2} \cdot t_2\) | ||||||||||||

\(\ds \) | \(\) | \(\, \ds + \, \) | \(\ds \map L {h, t_2} - \map C {h, t_1} \cdot u_1 \cdot \map R {f_1}\) |

and:

\(\ds g_2\) | \(=\) | \(\ds \map H {h, t_1} + \map C {h, t_1} \cdot t_1 + \map B {h, t_1, t_2} + 0 \cdot t_2\) | ||||||||||||

\(\ds \) | \(\) | \(\, \ds + \, \) | \(\ds \map L {h, t_2} - \map C {h, t_2} \cdot u_2 \cdot \map R {f_2}\) |

where:

- $u_1 := \dfrac {t_1} {\map {\operatorname {LPP} } {f_1} }$

and:

- $u_2 := \dfrac {t_2} {\map {\operatorname {LPP} } {f_1} }$

Furthermore:

\(\ds g_2 \to_{f_1} g_{1, 2}\) | \(=\) | \(\ds \map H {h, t_1} + 0 \cdot t_1 + \map B {h, t_1, t_2} + 0 \cdot t_2 + \map L {h, t_2}\) | ||||||||||||

\(\ds \) | \(\) | \(\, \ds - \, \) | \(\ds \map C {h, t_1} \cdot u_1 \cdot \map R {f_1} - \map C {h, t_2} \cdot u_2 \cdot \map R {f_2}\) |

Now:

- $g_1 = h - \map C {h, t_1} \cdot u_1 \cdot f_1$

and:

- $g_{1, 2} = g_2 - \map C {h, t_1} \cdot u_1 \cdot f_1$

and, by assumption:

- $h \to_F g_2$

Hence, by sum semi-compatibility:

- $g_1 \downarrow_{\stackrel * F} g_{1, 2}$

and hence:

- $g_1 \stackrel {\prec h} {\longleftrightarrow^*_F} g_2$

(Note that, in general, $g_1 \to_{f_1} g_{1, 2}$ need not be the case. Why not?)

This article, or a section of it, needs explaining.In particular: Not $\mathsf{Pr} \infty \mathsf{fWiki}$ style. Needs to be linked to a page demonstrating this fact.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

*Case $t_1 \prec t_2$*:

Analogous.

*Case $t := t_1 = t_2$*:

In this case:

- $g_1 = \map H {h, t} + 0 \cdot t + \map L {h, t} - \map C {h, t} \cdot u_1 \cdot \map R {f_1}$

and:

- $g_2 = \map H {h, t} + 0 \cdot t + \map L {h, t} - \map C {h, t} \cdot u_2 \cdot \map R {f_2}$

Hence:

\(\ds g_1 - g_2\) | \(=\) | \(\ds - \map C {h, t} \cdot \paren {u_1 \cdot \map R {f_1} - u_2 \cdot \map R {f_2} }\) | ||||||||||||

\(\ds \) | \(=\) | \(\ds - \map C {h, t} \cdot \paren {u_1 \cdot f_1 - u_2 \cdot f_2}\) | ||||||||||||

\(\ds \) | \(=\) | \(\ds - \map C {h, t} \cdot v \cdot \map {\operatorname {SP} } {f_1, f_2}\) |

This article, or a section of it, needs explaining.In particular: Explain why the above steps hold, by links to explanatory pages if necessaryYou can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

where:

- $v := t / \map {\operatorname {LCM} } {\map {\operatorname {LPP} } {f_1}, \map {\operatorname {LPP} } {f_2} }$

This article, or a section of it, needs explaining.In particular: Presumably here $\operatorname {LCM}$ means lowest common multiple?You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

We have assumed that:

- $\map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = 0$

That is:

- $\map {\operatorname {SP} } {f_1, f_2} \to_{\stackrel * F} 0$

Hence, by product compatibility:

- $g_1 - g_2 = - \map C {h, t} \cdot v \cdot \map {\operatorname {SP} } {f_1, f_2} \to_{\stackrel * F} 0$

This means that there exists a sequence $p \in P^*$ such that:

\(\ds p_1\) | \(=\) | \(\ds g_1 - g_2\) | ||||||||||||

\(\text {(1)}: \quad\) | \(\ds \forall 1 \le i < \size p: \, \) | \(\ds p_i\) | \(\to_F\) | \(\ds p_{i + 1}\) |

This article, or a section of it, needs explaining.In particular: What is $P^*$?You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

and:

- $p_{\size p} = 0 $

Furthermore note that, because of $\to_F \subseteq \succ$:

- $\forall 1 \le i < \size p: p_i\preceq g_1 -g_2 \prec h$

Thus, by sum semi-compatibility applied to $(1)$:

- $g_1 = p_1 + g_2$

- $\forall 1 \le i < \size p: p_i + g_2 \downarrow_{\stackrel * F} p_{i + 1} + g_2$

- $g_2 = p_{\size p} + g + 2$

Also, we have:

- $\forall 1 \le i < \size p: p_i + g_2 \prec h$

because:

- $\forall 1 \le i < \size p: \map H {p_i + g_2, t} = \map H {h, t} \wedge \map C {p_i + g_2, t} = 0$

Thus, summarizing:

- $g_1 \stackrel {\prec h} {\longleftrightarrow^*_F} g_2$ also in this case.

## Buchberger's Algorithm

This page has been identified as a candidate for refactoring of basic complexity.In particular: This algorithm needs to go on a separate page.Until this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

**Input**: a finite set of polynomials $F$

**Output**: $\map {\operatorname {GB} } F$, a Gröbner bases of $\map {\operatorname {Ideal} } F$

- $\map {\operatorname {Gröbner-Basis} } F := \map {\operatorname {GB} } {F, \set {f_1, f_2} | f_1, f_2 \in F}$
- $\map {\operatorname {GB} } {F, \O} := F$
- $\map {\operatorname {GB} } {F, \set {f_1, f_2} \cup B} := \begin{cases} \map {\operatorname {GB} } {F, B} & : h = 0 \\ \map {\operatorname {GB} } {F \cup h, B \cup \set {h, f | f \in F} } & : \text{otherwise} \end{cases}$

where:

- $h := \map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} }$

## Source of Name

This entry was named for Wolfgang Gröbner.

## Sources

- 1965: Bruno Buchberger:
*Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal*() (PhD thesis)

- 1970: Bruno Buchberger:
*An Algorithmic Criterion for the Solvability of a System of Algebraic Equations*(*Aequationes Mathematicae***Vol. 4**: pp. 374 – 383)

- 2006: Bruno Buchberger:
*An Algorithm for Finding the Basis Elements of the Residue Class Ring of a Zero Dimensional Polynomial Ideal*(*J. Symb. Comput.***Vol. 41**: pp. 471 – 511)

- (translated by Michael P. Abramson from "Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal")