Faugère’s F4 Algorithm Formalization

1 Gröbner Basis

Here we fix a field \(k\) of coefficients, and a monomial order \(\le \) on \(k[x_1, \cdots , x_n]\). Let \(f \in k[x_1, \cdots , x_n] \, \backslash \, \{ 0 \} \).

Definition 1 Monomial order
#

A monomial order on \(k[x_1, \cdots , x_n]\) is a total order \({\lt}\) on \(\mathbb {Z}_{\ge 0}^n\) satisfying:

  1. if \(\alpha {\lt} \beta \), then \(\alpha + \gamma {\lt} \beta + \gamma \) for any \(\gamma \in \mathbb {Z}_{\ge 0}^n\);

  2. \({\lt}\) is a well-ordering.

Definition 2 Leading monomial, leading coefficient, and leading term

The leading monomial \(\mathrm{LM}(f)\) of \(f\) is the monomial in \(f\) maximum under the fixed monomial order. The leading coefficient \(\mathrm{LC}(f)\) of \(f\) is the coefficient of \(\mathrm{LM}(f)\) in \(f\). The leading term of \(f\) is then simply the \(\mathrm{LC}(f)\)-multiple of \(\mathrm{LM}(f)\).

Definition 3 Monomial ideal
#

An ideal \(I \trianglelefteq k[x_1, \cdots , x_n]\) is a monomial ideal if there exists a subset of exponents \(A \subseteq \mathbb {Z}_{\ge 0}^n\) such that

\[ I = \langle x^\alpha : \alpha \in A \rangle . \]
Definition 4 Gröbner basis
#

A finite subset \(G = \{ g_1, \cdots , g_t \} \ne \{ 0 \} \) of \(I \trianglelefteq k[x_1, \cdots , x_n]\) is said to be a Gröbner basis of \(I\) if

\[ \langle \mathrm{LM}(I) \rangle = \langle \mathrm{LM}(G) \rangle = \langle \mathrm{LM}(g_1), \cdots , \mathrm{LM}(g_t) \rangle . \]