- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Let \(G = \{ g_1, \dots , g_t\} \) be a Gröbner basis for an ideal \(I \subseteq k[x_1, \dots , x_n]\) (with respect to a given monomial order \({\gt}\)) and let \(f \in k[x_1, \dots , x_n]\). Then \(f \in I\) if and only if the remainder on division of \(f\) by \(G\) is zero.
Let \((M,\le )\) be a preordered set. Define an equivalence relation
We write \([a]\) for the equivalence class of \(a\), and denote the quotient by
Fix a monomial order on \(k[x_1,\dots ,x_n]\) and let \(I \subseteq k[x_1,\dots ,x_n]\) be an ideal. A finite set \(G \subseteq I\) is called a Gröbner basis (or standard basis) for \(I\) if
\(0 \notin G\), and
- \[ \big\langle \, \operatorname {LT}(g)\ \big|\ g\in G \, \big\rangle \; =\; \big\langle \, \operatorname {LT}(f)\ \big|\ f\in I\setminus \{ 0\} \, \big\rangle . \]
We adopt the convention \(\langle \varnothing \rangle = (0)\), so that \(\varnothing \) is a Gröbner basis of the zero ideal.
Fix a monomial order on \(k[x_1,\dots ,x_n]\). Let \(I \subseteq k[x_1,\dots ,x_n]\) be an ideal and let \(G \subseteq k[x_1,\dots ,x_n]\) be a finite set.
We say that \(G\) satisfies the Gröbner basis property for \(I\) if
\(G \subseteq I\), and
the ideal generated by the leading terms of elements of \(G\) equals the leading term ideal of \(I\), i.e.
\[ \big\langle \, \operatorname {LT}(g)\ \big|\ g\in G \, \big\rangle \; =\; \big\langle \, \operatorname {LT}(f)\ \big|\ f\in I\setminus \{ 0\} \, \big\rangle . \]
Let \(I\subseteq k[x_1,\dots ,x_n]\) be an ideal, and fix a monomial ordering on \(k[x_1,\dots ,x_n]\). Then:
We denote by
\[ \mathrm{LT}(I) = \{ \, c\, x^\alpha \mid \exists \, f\in I\setminus \{ 0\} \text{ with }\mathrm{LT}(f)=c\, x^\alpha \} . \]\[ \mathrm{LM}(I) = \{ \, x^\alpha \mid \exists \, f\in I\setminus \{ 0\} \text{ with }\mathrm{LM}(f)=x^\alpha \} . \]We denote by \(\langle \mathrm{in}(I)\rangle \) the ideal generated by the elements of \(\mathrm{LM}(I)\).
Let \(N \subseteq M\). An element \(a \in N\) is called minimal in \(N\) if there is no \(b \in N\) such that \(b {\lt} a\) (where \({\lt}\) is the strict part of the quasi-order). We denote the set of all minimal elements of \(N\) by:
The min–classes of \(N\) are the intersections of \(N\) with the \(\sim \)-equivalence classes of its minimal elements:
An ideal \(I \subseteq k[x_1,\dots ,x_n]\) is called a monomial ideal if there is a subset \(A \subseteq \mathbb {Z}_{\ge 0}^n\) (possibly infinite) such that \(I\) consists of all polynomials which can be written as finite sums of the form
In this case we write
Let \(r\) be a relation on \(M\). Then \(r\) is called
reflexive if \(\Delta (M) \subseteq r\),
symmetric if \(r \subseteq r^{-1}\),
transitive if \(r \circ r \subseteq r\),
antisymmetric if \(r \cap r^{-1} \subseteq \Delta (M)\),
connex if \(r \cup r^{-1} = M \times M\),
irreflexive if \(\Delta (M) \cap r = \emptyset \),
strictly antisymmetric if \(r \cap r^{-1} = \emptyset \),
an equivalence relation on \(M\) if \(r\) is reflexive, symmetric, and transitive,
a quasi-order (preorder) on \(M\) if \(r\) is reflexive and transitive,
a partial order on \(M\) if \(r\) is reflexive, transitive and antisymmetric,
a (linear) order on \(M\) if \(r\) is a connex partial order on \(M\), and
a linear quasi-order on \(M\) if \(r\) is a connex quasi-order on \(M\).
A polyhedron \(Q\) which is bounded is called a polytope. Every polytope \(Q\) can be written as the convex hull of a finite set of points
Fix a monomial order and a set (or ordered tuple) \(B\) of polynomials with nonzero leading coefficients. 1 For each \(f\), choose one decomposition provided by the Division Algorithm:
where only finitely many coefficients \(q_b(f)\) are nonzero, and \(\operatorname {rem}(f,B)\) satisfies the remainder condition: either \(\operatorname {rem}(f,B)=0\), or it is a \(k\)-linear combination of monomials, none of which is divisible by \(\operatorname {LT}(b)\) for any \(b\in B\).
We call the finitely supported family \(q(f) = (q_b(f))_{b\in B}\) the quotients of \(f\) by \(B\), and we call \(\operatorname {rem}(f,B)\) the normal form (or remainder) of \(f\) on division by \(B\).
Fix a monomial order and let \(G = \left\{ g_1, \ldots , g_t\right\} \subseteq k[x_1, \ldots , x_n]\). Given \(f \in k[x_1, \ldots , x_n]\), we say that \(f\) reduces to zero modulo \(G\), written \(f \xrightarrow {G} 0\), if \(f\) has a standard representation
which means that whenever \(A_ig_i \neq 0\), we have
Let \(f,g\in k[x_1,\dots ,x_n]\) be nonzero polynomials.
If \(\operatorname {multideg}(f)=\alpha \) and \(\operatorname {multideg}(g)=\beta \), then let
\[ \gamma = (\gamma _1,\dots ,\gamma _n), \quad \gamma _i = \max (\alpha _i,\beta _i) \quad \text{for each }i. \]We call \(x^\gamma \) the least common multiple of \(\operatorname {LM}(f)\) and \(\operatorname {LM}(g)\), written
\[ x^\gamma \; =\; \operatorname {lcm}\bigl(\operatorname {LM}(f),\, \operatorname {LM}(g)\bigr). \]The \(S\)-polynomial of \(f\) and \(g\) is the combination
\[ S(f,g) \; =\; \frac{x^\gamma }{\mathrm{LT}(f)}\, f \; -\; \frac{x^\gamma }{\mathrm{LT}(g)}\, g. \]
Let \(r\) be a relation on \(M\) with strict part \(r_s\), and let \(N \subseteq M\).
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.
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}\).
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\).
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\).
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 \).
A well partial order, or a wpo, is a wqo that is a proper ordering relation, i.e., it is antisymmetric.
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:
where the \(\max \) is taken with respect to the monomial order.
Let \(I\) be an ideal and let \(G\) be a finite set of polynomials. Then \(G\) satisfies the Gröbner basis property for \(I\) if and only if \(G\setminus \{ 0\} \) satisfies the same property:
Let \(I=\langle x^\alpha \mid \alpha \in A\rangle \) be a monomial ideal in \(k[x_1,\dots ,x_n]\). For a polynomial \(f=\sum _{\gamma } c_\gamma x^\gamma \), write \(\operatorname {supp}(f)=\{ \gamma \mid c_\gamma \neq 0\} \). Then
equivalently, every monomial term \(x^\gamma \) appearing in \(f\) is divisible by some generator \(x^\alpha \) with \(\alpha \in A\).
Let \(N \subseteq M\) and let \(a \in N\). Consider the restricted subset
Then every min–class of \(N_{\le a}\) is also a min–class of \(N\), i.e.
Let \(s\) be a finite set of indices in \(\iota \), and let \(F \colon \iota \times \iota \to M\) where \(M\) is a commutative monoid. Assume that the diagonal values are all \(1\), i.e.
Then the product of \(F\) over the Cartesian product \(s\times s\) equals the product over the off-diagonal part:
With the notation of Definition 20, for every polynomial \(f\) we have:
Division equation:
\[ f \; =\; \sum _{b\in B} q_b(f)\, b \; +\; \operatorname {rem}(f,B). \]Degree control: for every \(b\in B\) with \(q_b(f)\neq 0\),
\[ \operatorname {multideg}(b\, q_b(f)) \; \preceq \; \operatorname {multideg}(f), \]where \(\operatorname {multideg}\) denotes multidegree with respect to the fixed monomial order.
Remainder condition: for every monomial \(x^\alpha \) appearing in \(\operatorname {rem}(f,B)\) with nonzero coefficient, and every \(b\in B\),
\[ \operatorname {LT}(b) \nmid x^\alpha . \]
Suppose we have a sum \(\sum _{i=1}^s p_i,\) where \(\operatorname {multideg}(p_i)=\delta \in \mathbb Z_{\ge 0}^n\) for all \(i\). If \(\operatorname {multideg}\Bigl(\sum _{i=1}^s p_i\Bigr){\lt}\delta ,\) then \(\sum _{i=1}^s p_i\) is a linear combination, with coefficients in \(k\), of the \(S\)-polynomials \(S(p_j,p_l)\quad \text{for }1\le j,\, l\le s\). Furthermore, each \(S(p_j,p_l)\) has multidegree \({\lt}\delta \).
Suppose that \(p_i = c_i x^{\alpha ^{(i)}} g_i\) and \(p_j = c_j x^{\alpha ^{(j)}} g_j\) have the same multidegree \(\delta \). Then
where \(x^{\gamma _{ij}} = \operatorname {lcm}(\operatorname {LM}(g_i), \operatorname {LM}(g_j))\).
Let \(s, t\) be finite sets of indices in \(\iota \), and let \(f \colon \iota \to A\) be a function to an additive commutative monoid. Then
Let \(s\) be a finite set of indices in \(\iota \), and let \(F \colon \iota \times \iota \to A\) where \(A\) is an additive commutative monoid. Assume that the diagonal values are all \(0\), i.e.
Then the sum of \(F\) over the Cartesian product \(s\times s\) equals the sum over the off-diagonal part:
Let \(I \subseteq k[x_1,\dots ,x_n]\) be an ideal and let \(G = \{ g_1,\dots ,g_t\} \) be a Gröbner basis for \(I\). Then given \(f \in k[x_1,\dots ,x_n]\) there is a unique \(r \in k[x_1,\dots ,x_n]\) with the following two properties:
No term of \(r\) is divisible by any of \(\mathrm{LT}(g_1),\dots ,\mathrm{LT}(g_t)\).
There is \(g\in I\) such that \(f = g + r\).
In particular, \(r\) is the remainder on division of \(f\) by \(G\) no matter how the elements of \(G\) are listed when using the division algorithm.
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\).
Let \(\preceq \) be a quasi-order on \(M\) with associated equivalence relation \(\sim \). Then the following are equivalent:
\(\preceq \) is a well-quasi-order.
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\).
For every nonempty subset \(N\) of \(M\), the number of min-classes in \(N\) is finite and non-zero.
Let \(I = \langle f_1, \ldots , f_s \rangle \ne \{ 0\} \) be a polynomial ideal. Then a Gröbner basis for \(I\) can be constructed in a finite number of steps by the following algorithm:
Input : \(F = (f_1, \ldots , f_s)\)
Output : A Gröbner basis \(G = (g_1, \ldots , g_t)\) for \(I\), with \(F \subseteq G\)
\(G := F\)
REPEAT
\(G' := G\)
FOR each pair \(\{ p, q\} \), \(p \ne q\) in \(G'\) DO
\(r := \overline{S(p, q)}^{G'}\)
IF \(r \ne 0\) THEN \(G := G \cup \{ r\} \)
UNTIL \(G = G'\)
RETURN \(G\)
Let \(I\) be a polynomial ideal in \(k[x_1, \dots , x_n]\). Then a basis \(G = \{ g_1, \dots , g_t\} \) of \(I\) is a Gröbner basis for \(I\) (with respect to a given monomial order \({\gt}\)) if and only if for all pairs \(i \neq j\), the remainder on division of the \(S\)-polynomial \(S(g_i, g_j)\) by \(G\) (listed in some order) is zero.
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
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.
Let \(P\) be a subset of \(K[X]\) and \(f\in K[X]\). Then there exists a normal form \(g\in K[X]\) of \(f\) modulo \(P\) and a family \(\mathcal{F}=\{ q_{p}\} _{p\in P}\) of elements of \(K[X]\) with
If \(P\) is finite, the ground field is computable, and the term order on \(T\) is decidable, then \(g\) and \(\{ q_{p}\} _{p\in P}\) can be computed from \(f\) and \(P\).
Let \(I \subseteq k[x_1, \ldots , x_n]\) be an ideal.
\(\langle \operatorname {LT}(I)\rangle \) is a monomial ideal.
There are \(g_1, \ldots , g_t \in I\) such that \(\langle \operatorname {LT}(I)\rangle = \langle \operatorname {LT}(g_1), \ldots , \operatorname {LT}(g_t)\rangle \).