theorem
MonomialOrder.exists_isGroebnerBasis
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
(I : Ideal (MvPolynomial σ k))
[Finite σ]
:
∃ (G : Finset (MvPolynomial σ k)), m.IsGroebnerBasis G I
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$.
theorem
MonomialOrder.groebner_basis_isRemainder_zero_iff_mem_span
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_4}
[CommRing R]
{p : MvPolynomial σ R}
{G : Finset (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)}
{r : MvPolynomial σ R}
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
(h : m.IsGroebnerBasis G I)
(hr : m.IsRemainder p (↑G) r)
:
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.
theorem
MonomialOrder.groebner_basis_isRemainder_zero_iff_mem_span₀
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{p : MvPolynomial σ R}
{G : Finset (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)}
{r : MvPolynomial σ R}
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0)
(h : m.IsGroebnerBasis G I)
(hr : m.IsRemainder p (↑G) r)
:
theorem
MonomialOrder.groebner_basis_isRemainder_zero_iff_mem_span'
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
{p : MvPolynomial σ k}
{G : Finset (MvPolynomial σ k)}
{I : Ideal (MvPolynomial σ k)}
{r : MvPolynomial σ k}
(h : m.IsGroebnerBasis G I)
(hr : m.IsRemainder p (↑G) r)
:
theorem
MonomialOrder.groebner_basis_zero_isRemainder_iff_mem_ideal
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{p : MvPolynomial σ R}
{G : Finset (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)}
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
(h : m.IsGroebnerBasis G I)
:
theorem
MonomialOrder.groebner_basis_zero_isRemainder_iff_mem_ideal₀
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{p : MvPolynomial σ R}
{G : Finset (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)}
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0)
(h : m.IsGroebnerBasis G I)
:
theorem
MonomialOrder.groebner_basis_zero_isRemainder_iff_mem_ideal'
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
{p : MvPolynomial σ k}
{G : Finset (MvPolynomial σ k)}
{I : Ideal (MvPolynomial σ k)}
(h : m.IsGroebnerBasis G I)
:
theorem
MonomialOrder.remainder_zero
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_4}
[CommSemiring R]
(p : MvPolynomial σ R)
(hp : p ≠ 0)
(B : Set (MvPolynomial σ R))
(hB : ∀ b ∈ B, IsRegular (m.leadingCoeff b))
(h : m.IsRemainder p B 0)
:
theorem
MonomialOrder.remainder_zero₀
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_4}
[CommSemiring R]
(p : MvPolynomial σ R)
(hp : p ≠ 0)
(B : Set (MvPolynomial σ R))
(hB : ∀ b ∈ B, IsRegular (m.leadingCoeff b) ∨ b = 0)
(h : m.IsRemainder p B 0)
:
theorem
MonomialOrder.remainder_zero'
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
(p : MvPolynomial σ k)
(hp : p ≠ 0)
(B : Set (MvPolynomial σ k))
(h : m.IsRemainder p B 0)
:
theorem
MonomialOrder.span_groebner_basis
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{G : Finset (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)}
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
(h : m.IsGroebnerBasis G I)
:
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$.
theorem
MonomialOrder.isGroebnerBasis_iff_span_eq_and_degree_le
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
(G : Finset (MvPolynomial σ R))
(I : Ideal (MvPolynomial σ R))
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
:
theorem
MonomialOrder.isGroebnerBasis_iff
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
(G : Finset (MvPolynomial σ R))
(I : Ideal (MvPolynomial σ R))
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
:
theorem
MonomialOrder.isGroebnerBasis_iff₀
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
(G : Finset (MvPolynomial σ R))
(I : Ideal (MvPolynomial σ R))
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0)
:
theorem
MonomialOrder.isGroebnerBasis_span_leading_monomial_eq
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{G : Finset (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)}
(h : m.IsGroebnerBasis G I)
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
:
Ideal.span (m.leadingTerm '' ↑G) = Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' (↑I \ {0}))
theorem
MonomialOrder.isGroebnerBasis_unique_isRemainder
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{G : Finset (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)}
(h : m.IsGroebnerBasis G I)
(hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
(p : MvPolynomial σ R)
:
theorem
MonomialOrder.isGroebnerBasis_iff'
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
(G : Finset (MvPolynomial σ k))
(I : Ideal (MvPolynomial σ 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
theorem
MonomialOrder.sPolynomial_ne_zero
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
(f g : MvPolynomial σ R)
(h : m.sPolynomial f g ≠ 0)
:
theorem
MonomialOrder.sPolynomial_decomposition
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{d : m.syn}
{ι : Type u_4}
{B : Finset ι}
{g : ι → MvPolynomial σ R}
(hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
(hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d)
:
∃ (c : ι → ι → R), ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
Let $f, h_1, \dots, h_m \in k[\mathbf{x}] \setminus \{0\}$, and suppose $$f = c_1 h_1 + \cdots + c_m h_m, \quad \text{with } c_i \in k.$$ If $$\mathrm{lm}(h_1) = \mathrm{lm}(h_2) = \cdots = \mathrm{lm}(h_i) > \mathrm{lm}(f),$$ then $$f = \sum_{1 \leq i < j \leq m} c_{i,j} S(h_i, h_j), \quad c_{i,j} \in k.$$ Furthermore, if $S(h_i, h_j) \ne 0$, then $\mathrm{lm}(h_i) > \mathrm{lm}(S(h_i, h_j))$.
theorem
MonomialOrder.sPolynomial_decomposition'
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
{d : m.syn}
{ι : Type u_4}
{B : Finset ι}
(g : ι → MvPolynomial σ k)
(hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∨ g b = 0)
(hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d)
:
∃ (c : ι → ι → k), ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
theorem
MonomialOrder.isGroebnerBasis_iff_isRemainder_sPolynomial_zero
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
(G : Finset (MvPolynomial σ k))
:
m.IsGroebnerBasis G (Ideal.span ↑G) ↔ ∀ (g₁ g₂ : { x : MvPolynomial σ k // x ∈ G }), m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) (↑G) 0
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$.
theorem
MonomialOrder.buchberger_criterion
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
(G : Finset (MvPolynomial σ k))
:
m.IsGroebnerBasis G (Ideal.span ↑G) ↔ ∀ (g₁ g₂ : { x : MvPolynomial σ k // x ∈ G }), m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) (↑G) 0
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$.
theorem
MonomialOrder.isGroebnerBasis_iff_isRemainder_sPolynomial_zero'
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
(G : Finset (MvPolynomial σ k))
:
m.IsGroebnerBasis G (Ideal.span ↑G) ↔ ∀ (g₁ g₂ : { x : MvPolynomial σ k // x ∈ G }) (r : MvPolynomial σ k),
m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) (↑G) r → r = 0
theorem
MonomialOrder.buchberger_criterion'
{σ : Type u_1}
{m : MonomialOrder σ}
{k : Type u_2}
[Field k]
(G : Finset (MvPolynomial σ k))
:
m.IsGroebnerBasis G (Ideal.span ↑G) ↔ ∀ (g₁ g₂ : { x : MvPolynomial σ k // x ∈ G }) (r : MvPolynomial σ k),
m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) (↑G) r → r = 0
Alias of MonomialOrder.isGroebnerBasis_iff_isRemainder_sPolynomial_zero'.