2 Lemmas
Let \(f: \alpha \to \beta \) be a function and \(s \subseteq \alpha \) a subset with finite image \(f(s)\). Then there exists a finite subset \(s' \subseteq _{\text{fin}} s\) such that:
\(s' \subseteq s\) (subset relation)
\(f(s') = f(s)\) (image equality)
\(|s'| = |f(s)|\) (cardinality preservation)
0 is less then any σ →₀ ℕ w.r.t. monomial order.
A variant of IsRemainder without coercion of a Set (MvPolynomial σ R).
A variant of IsRemainder where g : MvPolynomial σ R →₀ MvPolynomial σ R is replaced with a function g : MvPolynomial σ R → MvPolynomial σ R without limitation on its support.
Remainders are preserved on insertion of the zero polynomial into the set of divisors.
Remainders are preserved with the zero polynomial removed from the set of divisors.
The leading term in a multivariate polynomial is zero if and only if this polynomial is zero.
the S-polynomial of \(f\) and \(g\) is antisymmetric:
For any polynomial \(g \in \operatorname{MvPolynomial}{\sigma }{R}\) and monomial order \(m\), the S-polynomial with zero as first argument vanishes:
For any polynomial \(g \in \operatorname{MvPolynomial}{\sigma }{R}\) and monomial order \(m\), the S-polynomial with zero as second argument vanishes:
Let \(G'' \subseteq R[\mathbf{X}]\) be a set of polynomials where every nonzero element has a unit leading coefficient:
Then for any polynomial \(p \in R[\mathbf{X}]\), there exists a remainder \(r\) satisfying:
where \(\operatorname{LC}_m(g)\) denotes the leading coefficient of \(g\) under monomial order \(m\).
\(h_1, h_2 \in k[\mathbf{x}], lm(h_1) = lm(h_2), S(h_1, h_2) \ne 0\), then \(lm(S(h_1, h_2)) {\lt} lm(h_1)\).
Monomial degree of product
Let \(k\) be a field, and let \(G'' \subseteq k[x_i : i \in \sigma ]\) be a set of polynomials. Then for any \(p \in k[x_i : i \in \sigma ]\), there exists a generalized remainder \(r\) of \(p\) upon division by \(G''\).
A subset \(s \subseteq R\) has finitely generated span if and only if: \(\exists \) finite \(s' \subseteq s\) such that \(\mathsf{span}(s) = \mathsf{span}(s')\)
For any ring \(R\), the span of the zero singleton set equals the zero submodule:
For any subset \(s \subseteq R\) of a ring \(R\), inserting zero does not change the linear span:
For any subset \(s \subseteq R\) of a ring \(R\), removing zero does not change the linear span:
Let \(G'' \subseteq R[x_1, \dots , x_n]\) be a set of polynomials such that
Then,
Let \(G'' \subseteq R[x_1, \dots , x_n]\), let \(I \subseteq R[x_1, \dots , x_n]\) be an ideal, and let \(p, r \in R[x_1, \dots , x_n]\). Suppose that:
\(G'' \subseteq I\),
\(r \in I\),
\(r\) is the remainder of \(p\) upon division by \(G''\).
Then,
Let \(R\) be a commutative ring, and let \(G'' \subseteq R[x_1, \dots , x_n]\), \(I \subseteq R[x_1, \dots , x_n]\) be an ideal, and \(p, r \in R[x_1, \dots , x_n]\). Assume that:
\(G'' \subseteq I\),
\(r\) is the remainder of \(p\) upon division by \(G''\).
Then,
Let \(I \subseteq k[x_i : i \in \sigma ]\) be an ideal, and let \(G \subseteq I\) be a finite subset. Suppose that \(r_1\) and \(r_2\) are generalized remainders of a polynomial \(p\) upon division by \(G\). Then,
Let \(I \subseteq k[x_1, \ldots , x_n]\) be an ideal. Then there exists a finite subset \(G = \{ g_1, \ldots , g_t\} \) of \(I\) such that \(G\) is a Gröbner basis for \(I\).
Let \(G = \{ g_1, \dots , g_t\} \) be a Gröbner basis for an ideal \(I \subseteq k[x_1, \dots , x_n]\) 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 \(G = \{ g_1, \ldots , g_t\} \) be a Gröbner basis for an ideal \(I \subseteq k[x_1, \ldots , x_n]\). Then \(G\) is a basis for the vector space \(I\) over \(k\).
Let \(G = \{ g_1, \ldots , g_t\} \) be a finite subset of \(k[x_1, \ldots , x_n]\). Then \(G\) is a Gröbner basis for the ideal \(I = \langle G \rangle \) if and only if for every \(f \in I\), the remainder of \(f\) on division by \(G\) is zero. whose leading coefficients are invertible with respect to a monomial order
Let \(f, h_1, \dots , h_m \in k[\mathbf{x}] \setminus \{ 0\} \), and suppose
If
then
Furthermore, if \(S(h_i, h_j) \ne 0\), then \(\mathrm{lm}(h_i) {\gt} \mathrm{lm}(S(h_i, h_j))\).
A basis \(G = \{ g_1, \ldots , g_t \} \) for an ideal \(I\) is a Gröbner basis if and only if \(S(g_i, g_j) \to _G 0\) for all \(i \neq j\).
Alias of MonomialOrder.isGroebnerBasis_iff_isRemainder_sPolynomial_zero.
A basis \(G = \{ g_1, \ldots , g_t \} \) for an ideal \(I\) is a Gröbner basis if and only if \(S(g_i, g_j) \to _G 0\) for all \(i \neq j\).
Alias of MonomialOrder.isGroebnerBasis_iff_isRemainder_sPolynomial_zero.