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)
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')\)
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\).
Given a remainder r of a polynomial p on division by a Gröbner basis G of an ideal I, the remainder r is 0 if and only if p is in the ideal I.
Any leading coefficient of polynomial in the Gröbner basis G is required to be a unit.
Formally:
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.
Given a remainder r of a polynomial p on division by a Gröbner basis G of an ideal I, the remainder r is 0 if and only if p is in the ideal I.
It is a variant of MonomialOrder.remainder_eq_zero_iff_mem_ideal_of_isGroebner, allowing the finite set to contain also 0, besides polynomials with invertible leading coefficients.
Given a remainder r of a polynomial p on division by a Gröbner basis G of an ideal I, the remainder r is 0 if and only if p is in the ideal I.
It is variant of MonomialOrder.remainder_eq_zero_iff_mem_ideal_of_isGroebner, over a field and without hypothesis on leading coefficients in the finite set.
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\).
A finite set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal and 0 is a remainder of each member of this ideal on division by this finite set.
Any leading coefficient of polynomial in the finite set is required to be a unit.
A finite set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal and 0 is a remainder of each member of this ideal on division by this finite set.
It is a variant of MonomialOrder.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero, allowing the finite set to contain also 0, besides polynomials with invertible leading coefficients.
A finite set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal and 0 is a remainder of each member of this ideal on division by this finite set.
It is a variant of MonomialOrder.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero, over a field and without hypothesis on leading coefficients in the finite set.
Formally:
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
Remainder of any polynomial on division by Gröbner basis exists and is unique.
Any leading coefficient of polynomial in the Gröbner basis is required to be a unit.
Remainder of any polynomial on division by Gröbner basis exists and is unique.
It is a variant of MonomialOrder.existsUnique_isRemainder_of_isGroebnerBasis, allowing the Gröbner basis to contain also 0, besides polynomials with invertible leading coefficients.
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.