Buchberger criterion

This file starts the formalization of Becker--Weispfenning--Kredel, Section 5.3.

The first result below is the reduction-theoretic core of Lemma 5.44: to prove that G is a Gröbner basis, it suffices to show that every one-step peak has reducts whose difference reduces to zero.

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

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

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

theorem MonomialOrder.isGroebnerBasis_span_iff_isGroebner {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (G : Set (MvPolynomial σ R)) : m.IsGroebnerBasis G (Ideal.span G) ↔ m.IsGroebner G

For the ideal generated by G, the ideal-based Gröbner basis definition is equivalent to the leading-term criterion for G itself.

theorem MonomialOrder.lTermReducesToPoly_C_leadingCoeff_mul_to_sPolynomial {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) (hdiv : m.degree g ≤ m.degree f) : m.LTermReducesToPoly g (MvPolynomial.C (m.leadingCoeff g) * f) (m.sPolynomial f g)

Becker--Weispfenning--Kredel, Exercise 5.47(iii).

If the leading term of g divides the leading term of f, then C (m.leadingCoeff g) * f top-reduces modulo g to the S-polynomial of f and g.

theorem MonomialOrder.monomial_mul_reducesToSet {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] (u : σ →₀ ℕ) {c : R} (hc : c ≠ 0) (P : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : m.ReducesToSet P f g) : m.ReducesToSet P ((MvPolynomial.monomial u) c * f) ((MvPolynomial.monomial u) c * g)

Multiplication by a nonzero monomial preserves one-step reduction modulo a set.

theorem MonomialOrder.monomial_mul_reflTransGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] (u : σ →₀ ℕ) (c : R) (P : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet P) f g) : Relation.ReflTransGen (m.ReducesToSet P) ((MvPolynomial.monomial u) c * f) ((MvPolynomial.monomial u) c * g)

Multiplication by a monomial preserves finite reduction modulo a set.

theorem MonomialOrder.monomial_mul_mem_reducesTo_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] (P : Set (MvPolynomial σ R)) {p : MvPolynomial σ R} (hpP : p ∈ P) (hp : p ≠ 0) (s : σ →₀ ℕ) {c : R} (hc : c * m.leadingCoeff p ≠ 0) : m.ReducesToSet P ((MvPolynomial.monomial s) c * p) 0

A monomial multiple of a member of P reduces to zero in one step, when its leading coefficient is nonzero.

theorem MonomialOrder.IsGroebner.of_localPeak_sub_reflTransGen_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) (hpeak : ∀ ⦃f f₁ f₂ : MvPolynomial σ R⦄, m.ReducesToSet G f f₁ → m.ReducesToSet G f f₂ → Relation.ReflTransGen (m.ReducesToSet G) (f₂ - f₁) 0) : m.IsGroebner G

Reduction-theoretic core of Becker--Weispfenning--Kredel, Lemma 5.44.

If every local peak f ⟶ f₁, f ⟶ f₂ has the property that f₂ - f₁ reduces to zero, then reduction modulo G is locally confluent; by Theorem 5.35, G is a Gröbner basis.

theorem MonomialOrder.IsGroebner.sPolynomial_reflTransGen_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) (hG : m.IsGroebner G) {g₁ g₂ : MvPolynomial σ R} (hg₁ : g₁ ∈ G) (hg₂ : g₂ ∈ G) : Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial g₁ g₂) 0

Theorem 5.48, forward implication.

If G is a Gröbner basis, then every S-polynomial of two elements of G reduces to zero modulo G.

theorem MonomialOrder.IsGroebner.normalForm_sPolynomial_eq_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) (hG : m.IsGroebner G) {g₁ g₂ h : MvPolynomial σ R} (hg₁ : g₁ ∈ G) (hg₂ : g₂ ∈ G) (hnf : Relation.IsNormalFormOf (m.ReducesToSet G) (m.sPolynomial g₁ g₂) h) : h = 0

Theorem 5.48, forward implication in normal-form form.

If G is a Gröbner basis, then every normal form of an S-polynomial of two elements of G is zero.

theorem MonomialOrder.IsGroebner.sPolynomial_reflTransGen_zero_of_normalForms_eq_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (hnf_zero : ∀ {g₁ g₂ h : MvPolynomial σ R}, g₁ ∈ G → g₂ ∈ G → Relation.IsNormalFormOf (m.ReducesToSet G) (m.sPolynomial g₁ g₂) h → h = 0) {g₁ g₂ : MvPolynomial σ R} (hg₁ : g₁ ∈ G) (hg₂ : g₂ ∈ G) : Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial g₁ g₂) 0

Theorem 5.48, implication (ii) → (iii).

If every normal form of each S-polynomial of pairs from G is zero, then each such S-polynomial reduces to zero.

theorem MonomialOrder.IsGroebner.of_sPolynomial_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] (G : Set (MvPolynomial σ R)) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (hspol : ∀ g₁ ∈ G, ∀ g₂ ∈ G, Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial g₁ g₂) 0) : m.IsGroebner G

Theorem 5.48, implication (iii) → (i).

If every S-polynomial of two elements of G reduces to zero modulo G, then G is a Gröbner basis.

theorem MonomialOrder.IsGroebner.iff_sPolynomial_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] (G : Set (MvPolynomial σ R)) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : m.IsGroebner G ↔ ∀ g₁ ∈ G, ∀ g₂ ∈ G, Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial g₁ g₂) 0

Theorem 5.48, equivalence of items (i) and (iii).

A set G is a Gröbner basis iff every S-polynomial of two elements of G reduces to zero modulo G.

theorem MonomialOrder.IsGroebnerBasis.sPolynomial_reflTransGen_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) (hGB : m.IsGroebnerBasis G I) {g₁ g₂ : MvPolynomial σ R} (hg₁ : g₁ ∈ G) (hg₂ : g₂ ∈ G) : Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial g₁ g₂) 0

Theorem 5.48, forward implication for the ideal-relative definition.

If G is a Gröbner basis of I, then every S-polynomial of two elements of G reduces to zero modulo G.

theorem MonomialOrder.IsGroebnerBasis.normalForm_sPolynomial_eq_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) (hGB : m.IsGroebnerBasis G I) {g₁ g₂ h : MvPolynomial σ R} (hg₁ : g₁ ∈ G) (hg₂ : g₂ ∈ G) (hnf : Relation.IsNormalFormOf (m.ReducesToSet G) (m.sPolynomial g₁ g₂) h) : h = 0

Theorem 5.48, normal-form forward implication for the ideal-relative definition.

If G is a Gröbner basis of I, then every normal form of an S-polynomial of two elements of G is zero.

theorem MonomialOrder.IsGroebnerBasis.of_sPolynomial_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) (hspan : Ideal.span G = I) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (hspol : ∀ g₁ ∈ G, ∀ g₂ ∈ G, Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial g₁ g₂) 0) : m.IsGroebnerBasis G I

Theorem 5.48, reverse implication for the ideal-relative definition.

If G generates I and every S-polynomial of two elements of G reduces to zero modulo G, then G is a Gröbner basis of I.

theorem MonomialOrder.IsGroebnerBasis.iff_sPolynomial_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) (hspan : Ideal.span G = I) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : m.IsGroebnerBasis G I ↔ ∀ g₁ ∈ G, ∀ g₂ ∈ G, Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial g₁ g₂) 0

Theorem 5.48, equivalence of items (i) and (iii) for an explicitly specified ideal I generated by G.