theorem MonomialOrder.exists_groebner_basis {σ : 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_3} [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) : r = 0 ↔ p ∈ 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.

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) : r = 0 ↔ p ∈ I

theorem MonomialOrder.groebner_basis_zero_isRemainder_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)} (hG' : ∀ g ∈ G', IsUnit (m.leadingCoeff g)) (h : m.IsGroebnerBasis G' I) : m.IsRemainder p (↑G') 0 ↔ p ∈ I

theorem MonomialOrder.groebner_basis_zero_isRemainder_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)} (h : m.IsGroebnerBasis G' I) : p ∈ I ↔ m.IsRemainder p (↑G') 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) : ∃ b ∈ B, b ≠ 0 ∧ m.degree b ≤ m.degree p

theorem MonomialOrder.IsGroebnerBasis_iff {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (G' : Finset (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k)) : m.IsGroebnerBasis G' I ↔ ↑G' ⊆ ↑I ∧ ∀ p ∈ I, m.IsRemainder p (↑G') 0

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.

theorem MonomialOrder.span_groebner_basis {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (G' : Finset (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k)) (h : m.IsGroebnerBasis G' I) : I = Ideal.span ↑G'

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.sPolynomial_decomposition {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (f : MvPolynomial σ k) (d : σ →₀ ℕ) (B : Finset (MvPolynomial σ k)) (c : MvPolynomial σ k → k) (hd : ∀ b ∈ B, m.degree b = d) (hfd : m.toSyn (m.degree f) < m.toSyn d) (hf : f = ∑ b ∈ B, c b • b) : ∃ (c' : MvPolynomial σ k → MvPolynomial σ k → k), f = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c' b₁ b₂ • m.sPolynomial b₁ 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_degree_lt {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (h₁ h₂ : MvPolynomial σ k) (h : m.degree h₁ = m.degree h₂) (hs : m.sPolynomial h₁ h₂ ≠ 0) : m.toSyn (m.degree (m.sPolynomial h₁ h₂)) < m.toSyn (m.degree h₁)

$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)) < lm(h_1)$.

theorem MonomialOrder.buchberger_criterion {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (G' : Finset (MvPolynomial σ k)) {g₁ g₂ : MvPolynomial σ k} (hG : ∀ (g₁ g₂ : { x : MvPolynomial σ k // x ∈ G' }), m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) (↑G') 0) : m.IsGroebnerBasis G' (Ideal.span ↑G')

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$.