Gröbner Basis

Definition:

• MonomialOrder.IsGroebnerBasis m G I: Given a monomial order m, a subset G of an ideal I is said to be a Gröbner basis if: (1) G is contained in I (i.e., all polynomials in G belong to the ideal I). (2) The ideal generated by the leading terms of all polynomials in I is equal to the ideal generated by the leading terms of the polynomials in G.

Buchberger criterion is proved with the following sequence of theorems, where each one is proved (directly or indirectly) with some of theorems before it:

• MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem_ideal: Given a remainder of a polynomial on division by a Gröbner basis of an ideal, the remainder is 0 if and only if the polynomial is in the ideal.

• MonomialOrder.IsGroebnerBasis.isRemainder_zero_iff_mem_ideal: Given a Gröbner basis of an ideal, 0 is a remainder of a polynomial on division by the Gröbner basis if and only if the polynomial is in the ideal I.

• MonomialOrder.IsGroebnerBasis.ideal_eq_span: Gröbner basis of any ideal spans the ideal.

• MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero: A 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 set.

• MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero (Buchberger Criterion): a basis of an ideal is a Gröbner basis of it if and only if 0 is a remainder of echo sPolynomial between two polynomials on the basis.

Other main theroems:

• MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder: Remainder of any polynomial on division by a Gröbner basis exists and is unique.

• MonomialOrder.IsGroebnerBasis.exists_isGroebnerBasis_finite: Finite Gröbner basis exists for any ideal of a noetherian multivariate polynomial ring.

Naming convention

Some theorems with an argument in type Set (MvPolynomial σ R) and a hypothesis that leading coefficients of all polynomials in the set are invertible have 2 variants, named as following respectively:

• without suffix ' or ₀: any polynomial b in the set has an invertible leading coefficient (IsUnit (m.leadingCoeff p));
• with suffix ₀: any polynomial b in the set either has an invertible leading coefficient or is equal to 0 (IsUnit (m.leadingCoeff p) ∨ b = 0);
• with suffix ': no hypotheses on leading coefficients, while requiring R to be a field (Field k, where the ring is denoted as k instead).

Reference : [Cox2015]

def MonomialOrder.IsGroebnerBasis {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) : Prop

A subset G of an ideal I is said to be a Gröbner basis if:

1. G is contained in I (i.e., all polynomials in G belong to the ideal I).
2. The ideal generated by the leading terms of all polynomials in I is equal to the ideal generated by the leading terms of the polynomials in G.

Equations

• MonomialOrder.IsGroebnerBasis G I = (G ⊆ ↑I ∧ Ideal.span (m.leadingTerm '' ↑I) = Ideal.span (m.leadingTerm '' G))

theorem MonomialOrder.IsGroebnerBasis.subset {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : IsGroebnerBasis G I) : G ⊆ ↑I

theorem MonomialOrder.IsGroebnerBasis.span_leadingTerm_image {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : IsGroebnerBasis G I) : Ideal.span (m.leadingTerm '' ↑I) = Ideal.span (m.leadingTerm '' G)

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) : IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ m.leadingTerm '' ↑I ⊆ ↑(Ideal.span (m.leadingTerm '' G))

theorem MonomialOrder.IsGroebnerBasis.of_subset {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G G' : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : IsGroebnerBasis G I) (hG : G ⊆ G') (hI : G' ⊆ ↑I) : IsGroebnerBasis G' I

@[simp]

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_self {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (I : Ideal (MvPolynomial σ R)) : IsGroebnerBasis (↑I) I

@[simp]

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_sdiff_singleton_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) : IsGroebnerBasis (G \ {0}) I ↔ IsGroebnerBasis G I

@[simp]

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_insert_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) : IsGroebnerBasis (insert 0 G) I ↔ IsGroebnerBasis G I

theorem MonomialOrder.IsGroebnerBasis.exists_isGroebnerBasis_finite {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [inst : IsNoetherianRing (MvPolynomial σ R)] (I : Ideal (MvPolynomial σ R)) : ∃ (G : Set (MvPolynomial σ R)), IsGroebnerBasis G I ∧ G.Finite

Finite Gröbner basis exists for any ideal of a noetherian multivariate polynomial ring.

theorem MonomialOrder.IsGroebnerBasis.singleton_zero_bot {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : IsGroebnerBasis {0} ⊥

theorem MonomialOrder.IsGroebnerBasis.empty_bot {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : IsGroebnerBasis ∅ ⊥

@[simp]

theorem MonomialOrder.IsGroebnerBasis.singleton_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (I : Ideal (MvPolynomial σ R)) : IsGroebnerBasis {0} I ↔ I = ⊥

@[simp]

theorem MonomialOrder.IsGroebnerBasis.empty_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (I : Ideal (MvPolynomial σ R)) : IsGroebnerBasis ∅ I ↔ I = ⊥

@[simp]

theorem MonomialOrder.IsGroebnerBasis.of_subsingleton {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Subsingleton (MvPolynomial σ R)] {s : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} : IsGroebnerBasis s I

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) : IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ ∀ p ∈ I, p ≠ 0 → ∃ g ∈ G, m.degree g ≤ m.degree p

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ ∀ p ∈ I, p ≠ 0 → ∃ g ∈ G, g ≠ 0 ∧ m.degree g ≤ m.degree p

theorem MonomialOrder.IsGroebnerBasis.span_leadingTerm_eq_span_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : 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.span_leadingTerm_eq_span_monomial₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : IsGroebnerBasis G I) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : Ideal.span (m.leadingTerm '' G) = Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' (↑I \ {0}))

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_of_forall_finite_isGroebnerBasis₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) {I : Ideal (MvPolynomial σ R)} (h : ∀ (s : Finset σ), ∃ (σ' : Type u_3) (m' : MonomialOrder σ') (e : m'.Embedding m), ↑s ⊆ Set.range ⇑e ∧ IsGroebnerBasis (⇑(MvPolynomial.rename ⇑e) ⁻¹' G) (Ideal.comap (MvPolynomial.rename ⇑e) I)) : IsGroebnerBasis G I

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_union_of_forall_finite_isGroebnerBasis₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {I : Ideal (MvPolynomial σ R)} {σ' : Finset σ → Type u_3} {m' : (s : Finset σ) → MonomialOrder (σ' s)} {e : (s : Finset σ) → (m' s).Embedding m} {G' : (s : Finset σ) → Set (MvPolynomial (σ' s) R)} (hG' : ∀ (s : Finset σ), ∀ g ∈ G' s, IsUnit ((m' s).leadingCoeff g) ∨ g = 0) (h : ∀ (s : Finset σ), ↑s ⊆ Set.range ⇑(e s)) (h' : ∀ (s : Finset σ), IsGroebnerBasis (G' s) (Ideal.comap (MvPolynomial.rename ⇑(e s)) I)) : IsGroebnerBasis (⋃ (s : Finset σ), ⇑(MvPolynomial.rename ⇑(e s)) '' G' s) I

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_of_forall_finite_isGroebnerBasis {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) {I : Ideal (MvPolynomial σ R)} (h : ∀ (s : Finset σ), ∃ (σ' : Type u_3) (m' : MonomialOrder σ') (e : m'.Embedding m), ↑s ⊆ Set.range ⇑e ∧ IsGroebnerBasis (⇑(MvPolynomial.rename ⇑e) ⁻¹' G) (Ideal.comap (MvPolynomial.rename ⇑e) I)) : IsGroebnerBasis G I

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_union_of_forall_finite_isGroebnerBasis {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {I : Ideal (MvPolynomial σ R)} {σ' : Finset σ → Type u_3} {m' : (s : Finset σ) → MonomialOrder (σ' s)} {e : (s : Finset σ) → (m' s).Embedding m} {G' : (s : Finset σ) → Set (MvPolynomial (σ' s) R)} (hG' : ∀ (s : Finset σ), ∀ g ∈ G' s, IsUnit ((m' s).leadingCoeff g)) (h : ∀ (s : Finset σ), ↑s ⊆ Set.range ⇑(e s)) (h' : ∀ (s : Finset σ), IsGroebnerBasis (G' s) (Ideal.comap (MvPolynomial.rename ⇑(e s)) I)) : IsGroebnerBasis (⋃ (s : Finset σ), ⇑(MvPolynomial.rename ⇑(e s)) '' G' s) I

theorem MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {p : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {r : MvPolynomial σ R} (h : IsGroebnerBasis G I) (hr : m.IsRemainder p G r) : r = 0 ↔ p ∈ 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.

theorem MonomialOrder.IsGroebnerBasis.isRemainder_zero_iff_mem_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {p : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) (h : IsGroebnerBasis G I) : m.IsRemainder p G 0 ↔ p ∈ I

Given a Gröbner basis G of an ideal I, 0 is a remainder on division by G if and only if p is in the ideal I.

theorem MonomialOrder.IsGroebnerBasis.isRemainder_zero_iff_mem_ideal₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {p : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (h : IsGroebnerBasis G I) : m.IsRemainder p G 0 ↔ p ∈ I

theorem MonomialOrder.IsGroebnerBasis.ideal_eq_span {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) (h : IsGroebnerBasis G I) : I = Ideal.span G

Gröbner basis of any ideal spans the ideal.

theorem MonomialOrder.IsGroebnerBasis.ideal_eq_span₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (h : IsGroebnerBasis G I) : I = Ideal.span G

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) : IsGroebnerBasis G I ↔ I = Ideal.span G ∧ IsGroebnerBasis G (Ideal.span G)

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : IsGroebnerBasis G I ↔ I = Ideal.span G ∧ IsGroebnerBasis G (Ideal.span G)

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) : IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ ∀ p ∈ I, m.IsRemainder p G 0

A 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 set.

Any leading coefficient of polynomial in the set is required to be a unit.

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ ∀ p ∈ I, m.IsRemainder p G 0

A 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 set.

It is a variant of MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero, allowing the set to contain also 0, besides polynomials with invertible leading coefficients.

theorem MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : IsGroebnerBasis G I) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) (p : MvPolynomial σ R) : ∃! r : MvPolynomial σ R, m.IsRemainder p G r

Remainder of any polynomial on division by a Gröbner basis exists and is unique.

Any leading coefficient of polynomial in the Gröbner basis is required to be a unit.

theorem MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : IsGroebnerBasis G I) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (p : MvPolynomial σ R) : ∃! r : MvPolynomial σ R, m.IsRemainder p G r

Remainder of any polynomial on division by a Gröbner basis exists and is unique.

It is a variant of MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder, allowing the Gröbner basis to contain also 0, besides polynomials with invertible leading coefficients.

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) : IsGroebnerBasis G (Ideal.span G) ↔ ∀ (g₁ g₂ : ↑G), m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) G 0

Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if 0 is a remainder of echo sPolynomial between two polynomials on the basis.

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : IsGroebnerBasis G (Ideal.span G) ↔ ∀ (g₁ g₂ : ↑G), m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) G 0

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_forall_isRemainder_sPolynomial_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) : IsGroebnerBasis G (Ideal.span G) ↔ ∀ (g₁ g₂ : ↑G) (r : MvPolynomial σ R), m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) G r → r = 0

Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if any remainder of echo sPolynomial between two polynomials on the basis is 0.

It is a variant of MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero.

theorem MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename {σ : Type u_1} {R : Type u_2} [CommRing R] {σ' : Type u_3} {m' : MonomialOrder σ'} {m : MonomialOrder σ} (e : m'.Embedding m) (G : Set (MvPolynomial σ' R)) (hG : ∀ g ∈ G, IsUnit (m'.leadingCoeff g)) (I : Ideal (MvPolynomial σ' R)) : IsGroebnerBasis G I ↔ IsGroebnerBasis (⇑(MvPolynomial.rename ⇑e) '' G) (Ideal.map (MvPolynomial.rename ⇑e) I)

theorem MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename₀ {σ : Type u_1} {R : Type u_2} [CommRing R] {σ' : Type u_3} {m' : MonomialOrder σ'} {m : MonomialOrder σ} (e : m'.Embedding m) (G : Set (MvPolynomial σ' R)) (hG : ∀ g ∈ G, IsUnit (m'.leadingCoeff g) ∨ g = 0) (I : Ideal (MvPolynomial σ' R)) : IsGroebnerBasis G I ↔ IsGroebnerBasis (⇑(MvPolynomial.rename ⇑e) '' G) (Ideal.map (MvPolynomial.rename ⇑e) I)

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

A 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 set.

It is a variant of MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero, over a field and without hypothesis on leading coefficients in the set.

theorem MonomialOrder.IsGroebnerBasis.isRemainder_zero_iff_mem_ideal' {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} {p : MvPolynomial σ k} {G : Set (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)} (h : IsGroebnerBasis G I) : m.IsRemainder p G 0 ↔ p ∈ I

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero' {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} (G : Set (MvPolynomial σ k)) : IsGroebnerBasis G (Ideal.span G) ↔ ∀ (g₁ g₂ : ↑G) (r : MvPolynomial σ k), m.IsRemainder (m.sPolynomial ↑g₁ ↑g₂) G r → r = 0

Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if any remainder of echo sPolynomial between two polynomials on the basis is 0.

It is a variant of MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero.

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span' {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} (G : Set (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k)) : IsGroebnerBasis G I ↔ I = Ideal.span G ∧ IsGroebnerBasis G (Ideal.span G)

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le' {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} (G : Set (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k)) : IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ ∀ p ∈ I, p ≠ 0 → ∃ g ∈ G, g ≠ 0 ∧ m.degree g ≤ m.degree p

theorem MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename' {k : Type u_1} [Field k] {σ : Type u_2} {σ' : Type u_3} {m' : MonomialOrder σ'} {m : MonomialOrder σ} (e : m'.Embedding m) (G : Set (MvPolynomial σ' k)) (I : Ideal (MvPolynomial σ' k)) : IsGroebnerBasis G I ↔ IsGroebnerBasis (⇑(MvPolynomial.rename ⇑e) '' G) (Ideal.map (MvPolynomial.rename ⇑e) I)

theorem MonomialOrder.IsGroebnerBasis.exists_isGroebnerBasis_finite_of_exists_span_finite {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} {B : Set (MvPolynomial σ k)} (hB : B.Finite) : ∃ (G : Set (MvPolynomial σ k)), IsGroebnerBasis G (Ideal.span B) ∧ G.Finite

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_of_forall_finite_isGroebnerBasis' {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} {G : Set (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)} (h : ∀ (s : Finset σ), ∃ (σ' : Type u_3) (m' : MonomialOrder σ') (e : m'.Embedding m), ↑s ⊆ Set.range ⇑e ∧ IsGroebnerBasis (⇑(MvPolynomial.rename ⇑e) ⁻¹' G) (Ideal.comap (MvPolynomial.rename ⇑e) I)) : IsGroebnerBasis G I

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_union_of_forall_finite_isGroebnerBasis' {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} {I : Ideal (MvPolynomial σ k)} {σ' : Finset σ → Type u_3} {m' : (s : Finset σ) → MonomialOrder (σ' s)} {e : (s : Finset σ) → (m' s).Embedding m} {G' : (s : Finset σ) → Set (MvPolynomial (σ' s) k)} (h : ∀ (s : Finset σ), ↑s ⊆ Set.range ⇑(e s)) (h' : ∀ (s : Finset σ), IsGroebnerBasis (G' s) (Ideal.comap (MvPolynomial.rename ⇑(e s)) I)) : IsGroebnerBasis (⋃ (s : Finset σ), ⇑(MvPolynomial.rename ⇑(e s)) '' G' s) I

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_minimal {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} (I : Ideal (MvPolynomial σ k)) {G : Set (MvPolynomial σ k)} : IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ {a : σ →₀ ℕ | Minimal (fun (x : σ →₀ ℕ) => x ∈ m.degree '' (↑I \ {0})) a} ⊆ m.degree '' (G \ {0})