Gröbner Basis

== Theorem ==
Let $F$ be a finite set of polynomials.
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 :
:$\forall f_1, f_2 \in \map F {\map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = 0}$
== 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$
By the relation between reduction and congruence this implies that:
:$\map {\operatorname {SP} } {f_1, f_2} \leftrightarrow_F^* 0$
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).
=== 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$
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:
and:
where:
: $u_1 := \dfrac {t_1} {\map {\operatorname {LPP} } {f_1} }$
and:
: $u_2 := \dfrac {t_2} {\map {\operatorname {LPP} } {f_1} }$
Furthermore:
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?)
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:
where:
:$v := t / \map {\operatorname {LCM} } {\map {\operatorname {LPP} } {f_1}, \map {\operatorname {LPP} } {f_2} }$
 
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:
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 ==
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} }$
== Sources ==
* (PhD thesis)
* 
* 
*