Buchberger Algorithm Formalization

2 Orders and Abstract Reduction Relations

2.1 Monomial Ideals and Dickson’s Lemma

Definition 3
#

Let \(r\) be a relation on \(M\). Then \(r\) is called

  1. reflexive if \(\Delta (M) \subseteq r\),

  2. symmetric if \(r \subseteq r^{-1}\),

  3. transitive if \(r \circ r \subseteq r\),

  4. antisymmetric if \(r \cap r^{-1} \subseteq \Delta (M)\),

  5. connex if \(r \cup r^{-1} = M \times M\),

  6. irreflexive if \(\Delta (M) \cap r = \emptyset \),

  7. strictly antisymmetric if \(r \cap r^{-1} = \emptyset \),

  8. an equivalence relation on \(M\) if \(r\) is reflexive, symmetric, and transitive,

  9. a quasi-order (preorder) on \(M\) if \(r\) is reflexive and transitive,

  10. a partial order on \(M\) if \(r\) is reflexive, transitive and antisymmetric,

  11. a (linear) order on \(M\) if \(r\) is a connex partial order on \(M\), and

  12. a linear quasi-order on \(M\) if \(r\) is a connex quasi-order on \(M\).

Definition 4
#

Let \(r\) be a relation on \(M\) with strict part \(r_s\), and let \(N \subseteq M\).

  1. Then an element \(a\) of \(N\) is called \(r\)-minimal (\(r\)-maximal) in \(N\) if there is no \(b \in N\) with \(b \, r_s \, a\) (with \(a \, r_s \, b\)). For \(N = M\) the reference to \(N\) is omitted.

  2. A strictly descending (strictly ascending) \(r\)-chain in \(M\) is an infinite sequence \(\{ a_n\} _{n \in \mathbb {N}}\) of elements of \(M\) such that \(a_{n+1} \, r_s \, a_n\) (such that \(a_n \, r_s \, a_{n+1}\)) for all \(n \in \mathbb {N}\).

  3. The relation \(r\) is called well-founded (noetherian) if every non-empty subset \(N\) of \(M\) has an \(r\)-minimal (an \(r\)-maximal) element. \(r\) is a well-order on \(M\) if \(r\) is a well-founded linear order on \(M\).

Definition 5 The “Antisymmetrization” of \(M\)
#

Let \((M,\le )\) be a preordered set. Define an equivalence relation

\[ \sim \; \colon \; M\times M\; \to \; \mathrm{Prop}, \qquad a\sim b \; \iff \; \bigl(a\le b \wedge b\le a\bigr). \]

We write \([a]\) for the equivalence class of \(a\), and denote the quotient by

\[ \mathrm{Quot}(M,\sim )\; =\; \{ \, [a]\mid a\in M\} . \]
Definition 6 Minimal elements and min–classes
#

Let \(N\subseteq M\). An element \(b\in N\) is called minimal in \(N\) if

\[ \forall \, y\in N,\; y\le b \; \Longrightarrow \; b\le y. \]

We denote by

\[ \operatorname {Minimal}(N) \; =\; \{ \, b\in N \mid \forall \, y\in N,\; y\le b\to b\le y\} \]

the set of all minimal elements of \(N\). The min–classes of \(N\) are then

\[ \operatorname {minClasses}(N) \; =\; \bigl\{ \, [b]\in \mathrm{Quot}(M,\sim )\; \bigm |\; b\in \operatorname {Minimal}(N)\bigr\} . \]
Definition 7
#

Let \(\preceq \) be a quasi-order on \(M\) and let \(N \subseteq M\). Then a subset \(B\) of \(N\) is called a Dickson basis, or simply basis of \(N\) w.r.t. \(\preceq \), if for every \(a \in N\) there exists some \(b \in B\) with \(b \preceq a\).

  1. We say that \(\preceq \) has the Dickson property, or is a well-quasi-order(wqo), if every subset \(N\) of \(M\) has a finite basis w.r.t. \(\preceq \).

  2. A well partial order, or a wpo, is a wqo that is a proper ordering relation, i.e., it is antisymmetric.

Let \(\preceq \) be a quasi-order on \(M\) with associated equivalence relation \(\sim \). Then the following are equivalent:

  1. \(\preceq \) is a well-quasi-order.

  2. Whenever \(\{ a_n\} _{n \in \mathbb {N}}\) is a sequence of elements of \(M\), then there exist \(i {\lt} j\) with \(a_i \preceq a_j\).

  3. For every nonempty subset \(N\) of \(M\), the number of min-classes in \(N\) is finite and non-zero.

Proof
Proposition 9

Let \(\preceq \) be a well- quasi-order on \(M\), and let \(\{ a_n\} _{n \in \mathbb {N}}\) be a sequence of elements of \(M\). Then there exists a strictly ascending sequence \(\{ n_i\} _{i \in \mathbb {N}}\) of natural numbers such that \(a_{n_i} \preceq a_{n_j}\) for all \(i {\lt} j\).

Proof

We define the sequence \(\{ n_i\} _{i \in \mathbb {N}}\) recursively, and by simultaneous induction on \(i\) we verify the following properties:

  1. \(a_{n_i} \preceq a_{n_{i+1}}\) for all \(i \in \mathbb {N}\), and

  2. for all \(i \in \mathbb {N}\), the set \(\{ n \in \mathbb {N} \mid a_{n_i} \preceq a_n\} \) is infinite.

For \(i=0\), let \(\{ b_1, \dots , b_k\} \) be a finite basis of the set \(\{ a_n \mid n \in \mathbb {N}\} \), and for each \(j\) with \(1 \le j \le k\), set

\[ B_j = \{ n \in \mathbb {N} \mid b_j \preceq a_n\} . \]

Then \(\bigcup _{j=1}^k B_j = \mathbb {N}\) by the choice of \(B\). Since the union of finitely many finite sets is finite, we can find a \(B_j\) which is infinite. Moreover, \(b_j = a_m\) for some \(m \in \mathbb {N}\), and we set \(n_0 = m\). For \(i+1\), we consider the set

\[ U_i = \{ a_n \mid a_{n_i} \preceq a_n, n_i {\lt} n\} . \]

By condition (ii) for \(i\), the set \(\{ n \in \mathbb {N} \mid a_n \in U_i\} \) is infinite. Choosing some finite basis of \(U_i\), we can, as before, find an element \(a_m\) in this basis such that \(a_m \preceq a_n\) for infinitely many different \(n \in \mathbb {N}\), and we take \(n_{i+1} = m\). Conditions (i) and (ii) obviously continue to hold. It now follows easily from condition (i) and the transitivity of \(\preceq \) that \(\{ n_i\} _{i \in \mathbb {N}}\) has the desired property.

Lemma 10
#

Let \(f, g \in k[x_1, \dots , x_n]\) be nonzero polynomials. Then:

  1. \(\operatorname {multideg}(fg) = \operatorname {multideg}(f) + \operatorname {multideg}(g)\).

  2. If \(f + g \neq 0\), then \(\operatorname {multideg}(f + g) \le \max (\operatorname {multideg}(f), \operatorname {multideg}(g))\). If, in addition, \(\operatorname {multideg}(f) \neq \operatorname {multideg}(g)\), then equality occurs.

Lemma 11
#

Let \(\iota \) be an index set and \(s \subset \iota \) a finite subset. For each \(i \in s\), let \(h_i \in k[x_1,\dots ,x_n]\). Then the following inequality holds:

\[ \operatorname {multideg}\left(\sum _{i \in s} h_i\right) \le \max _{i \in s} \left\{ \operatorname {multideg}(h_i) \right\} \]

where the \(\max \) is taken with respect to the monomial order.

Proof

Let \(M = \max _{i \in s} \{ \operatorname {multideg}(h_i) \} \). Any monomial \(x^b\) appearing in the sum \(\sum _{i \in s} h_i\) must be a monomial in at least one of the summands, say \(h_{i_0}\) for some \(i_0 \in s\). By definition, the multidegree of any such term is bounded by the multidegree of the polynomial it belongs to, so \(b \le \operatorname {multideg}(h_{i_0})\). Also by definition, \(\operatorname {multideg}(h_{i_0}) \le M\). Therefore, \(b \le M\) for any monomial \(x^b\) in the sum. This implies that the multidegree of the sum itself cannot exceed \(M\).

Lemma 12

Let \(I = \langle x^\alpha \mid \alpha \in A \rangle \) be a monomial ideal. Then a monomial \(x^\beta \) lies in \(I\) if and only if \(x^\beta \) is divisible by \(x^\alpha \) for some \(\alpha \in A\).

Proof

If \(x^\beta \) is a multiple of \(x^\alpha \) for some \(\alpha \in A\), then \(x^\beta \in I\) by the definition of ideal. Conversely, if \(x^\beta \in I\), then \(x^\beta = \sum _{i=1}^s h_i x^{\alpha (i)}\), where \(h_i \in k[x_1, \dots , x_n]\) and \(\alpha (i) \in A\). If we expand each \(h_i\) as a sum of terms, we obtain

\[ x^\beta = \sum _{i=1}^s h_i x^{\alpha (i)} = \sum _{i=1}^s \left(\sum _j c_{i,j} x^{\beta (i,j)}\right) x^{\alpha (i)} = \sum _{i,j} c_{i,j} x^{\beta (i,j)} x^{\alpha (i)}. \]
Theorem 13

Let \((\mathbb {N}^n, \le ')\) be the direct product of \(n\) copies of the natural numbers \((\mathbb {N}, \le )\) with their natural ordering. Then \((\mathbb {N}^n, \le ')\) is a Dickson partially ordered set. More explicitly, every subset \(S \subseteq \mathbb {N}^n\) has a finite subset \(B\) such that for every \((m_1, \dots , m_n) \in S\), there exists \((k_1, \dots , k_n) \in B\) with

\[ k_i \le m_i \quad \text{for } 1 \le i \le n. \]
Proof
Theorem 14 Dickson’s Lemma (MvPolynomial)
#

Let \(I = \langle x^{\alpha } | \alpha \in A \rangle \subseteq k[x_1, \ldots , x_n]\) be a monomial ideal. Then \(I\) can be written in the form \(I = \langle x^{\alpha (1)}, \ldots , {\alpha (s)} \rangle \), where \(\alpha (1), \ldots , \alpha (s) \in A\). In particular, \(I\) has a finite basis.

Proof