An abstract Buchberger procedure

This file starts the formalization of Becker--Weispfenning--Kredel, Theorem 5.53.

The procedure is represented by an abstract step relation on sets of polynomials: choose a pair from the current set, reduce its S-polynomial to a nonzero normal form with unit leading coefficient, and add that normal form to the set.

The correctness theorem in this file says that any set reached by such steps that satisfies the S-polynomial condition is a Gröbner basis of the ideal generated by the initial set. Over a Noetherian polynomial ring, every state reaches a terminal state. Over a field with finitely many variables, finite initial sets reach finite terminal sets.

noncomputable def MonomialOrder.leadingTermIdeal {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) : Ideal (MvPolynomial σ R)

The ideal generated by the leading terms of the elements of G.

Equations

• m.leadingTermIdeal G = Ideal.span (m.leadingTerm '' G)

def MonomialOrder.BuchbergerStep {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G H : Set (MvPolynomial σ R)) : Prop

One abstract Buchberger step.

The next set is obtained by adjoining a nonzero normal form of an S-polynomial of two current generators. The unit leading coefficient assumption is included so that the existing reduction API over general coefficient rings remains available after adjoining the new polynomial.

Equations

• One or more equations did not get rendered due to their size.

def MonomialOrder.SPolynomialCondition {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) : Prop

The S-polynomial condition: every S-polynomial of two elements reduces to zero modulo the set.

Equations

• m.SPolynomialCondition G = ∀ p ∈ G, ∀ q ∈ G, Relation.ReflTransGen (m.ReducesToSet G) (m.sPolynomial p q) 0

theorem MonomialOrder.BuchbergerStep.span_eq {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : Set (MvPolynomial σ R)} (hstep : m.BuchbergerStep G H) : Ideal.span H = Ideal.span G

theorem MonomialOrder.BuchbergerStep.finite {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : Set (MvPolynomial σ R)} (hstep : m.BuchbergerStep G H) (hG : G.Finite) : H.Finite

One abstract Buchberger step preserves finiteness of the polynomial set.

theorem MonomialOrder.BuchbergerStep.leadingCoeff_condition {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : Set (MvPolynomial σ R)} (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (hstep : m.BuchbergerStep G H) (h : MvPolynomial σ R) : h ∈ H → IsUnit (m.leadingCoeff h) ∨ h = 0

theorem MonomialOrder.BuchbergerStep.not_leadingTerm_mem_leadingTermIdeal_of_isNormalForm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) {h : MvPolynomial σ R} (hh : h ≠ 0) (hnf : Relation.IsNormalForm (m.ReducesToSet G) h) : m.leadingTerm h ∉ m.leadingTermIdeal G

theorem MonomialOrder.BuchbergerStep.leadingTermIdeal_lt {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : Set (MvPolynomial σ R)} (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (hstep : m.BuchbergerStep G H) : m.leadingTermIdeal G < m.leadingTermIdeal H

theorem MonomialOrder.IsGroebnerBasis.of_sPolynomialCondition {σ : 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) (hcondition : m.SPolynomialCondition G) : m.IsGroebnerBasis G I

theorem MonomialOrder.ReflTransGen_BuchbergerStep.span_eq {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : Set (MvPolynomial σ R)} (hsteps : Relation.ReflTransGen m.BuchbergerStep G H) : Ideal.span H = Ideal.span G

theorem MonomialOrder.ReflTransGen_BuchbergerStep.finite {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : Set (MvPolynomial σ R)} (hsteps : Relation.ReflTransGen m.BuchbergerStep G H) (hG : G.Finite) : H.Finite

A finite sequence of abstract Buchberger steps preserves finiteness.

theorem MonomialOrder.ReflTransGen_BuchbergerStep.leadingCoeff_condition {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : Set (MvPolynomial σ R)} (hsteps : Relation.ReflTransGen m.BuchbergerStep G H) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (h : MvPolynomial σ R) : h ∈ H → IsUnit (m.leadingCoeff h) ∨ h = 0

theorem MonomialOrder.IsGroebnerBasis.of_buchbergerSteps_of_sPolynomialCondition {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] {G H : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hsteps : Relation.ReflTransGen m.BuchbergerStep G H) (hspan : Ideal.span G = I) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (hcondition : m.SPolynomialCondition H) : m.IsGroebnerBasis H I

Correctness of the abstract Buchberger procedure.

If H is reached from G by Buchberger steps and satisfies the S-polynomial condition, then H is a Gröbner basis of the original ideal I.

def MonomialOrder.BuchbergerState {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] : Type (max u_1 u_2)

States for the abstract Buchberger procedure over a general coefficient ring. The invariant records that every current generator is either zero or has unit leading coefficient.

Equations

• m.BuchbergerState = { G : Set (MvPolynomial σ R) // ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0 }

def MonomialOrder.BuchbergerState.Step {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G H : m.BuchbergerState) : Prop

The step relation on Buchberger states.

Equations

• MonomialOrder.BuchbergerState.Step m G H = m.BuchbergerStep ↑G ↑H

theorem MonomialOrder.BuchbergerState.step_leadingTermIdeal_lt {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {G H : m.BuchbergerState} (hstep : Step m G H) : m.leadingTermIdeal ↑G < m.leadingTermIdeal ↑H

theorem MonomialOrder.BuchbergerState.wellFounded_flip {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [IsNoetherianRing (MvPolynomial σ R)] : WellFounded (flip (Step m))

Noetherian termination for the abstract Buchberger step relation.

This is the ACC argument underlying Buchberger's algorithm: every genuine step strictly increases the leading-term ideal, and this cannot happen indefinitely in a Noetherian polynomial ring.

def MonomialOrder.BuchbergerState.Terminal {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : m.BuchbergerState) : Prop

A terminal state has no outgoing Buchberger step.

Equations

• MonomialOrder.BuchbergerState.Terminal m G = ∀ (H : m.BuchbergerState), ¬MonomialOrder.BuchbergerState.Step m G H

theorem MonomialOrder.BuchbergerState.exists_terminal {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [IsNoetherianRing (MvPolynomial σ R)] (G : m.BuchbergerState) : ∃ (H : m.BuchbergerState), Relation.ReflTransGen (Step m) G H ∧ Terminal m H

Every state reaches a terminal state in a Noetherian polynomial ring.

theorem MonomialOrder.BuchbergerState.sPolynomialCondition_of_terminal {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (hunit : ∀ (f : MvPolynomial σ R), f ≠ 0 → IsUnit (m.leadingCoeff f)) {G : m.BuchbergerState} (hterm : Terminal m G) : m.SPolynomialCondition ↑G

If every nonzero polynomial has unit leading coefficient, then a terminal Buchberger state satisfies the S-polynomial condition.

This hypothesis is automatic over fields, and it is the point where the general coefficient-ring version needs a coefficient condition beyond Noetherianity.

theorem MonomialOrder.BuchbergerState.exists_isGroebnerBasis_terminal {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] [NoZeroDivisors R] [IsNoetherianRing (MvPolynomial σ R)] (hunit : ∀ (f : MvPolynomial σ R), f ≠ 0 → IsUnit (m.leadingCoeff f)) {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hspan : Ideal.span G = I) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : ∃ (H : m.BuchbergerState), Relation.ReflTransGen (Step m) ⟨G, hG₀⟩ H ∧ Terminal m H ∧ m.IsGroebnerBasis (↑H) I

Existence and correctness of a terminal abstract Buchberger run.

Starting from G, the abstract procedure reaches a terminal state H; if nonzero normal forms have unit leading coefficient, then H is a Gröbner basis of the original ideal I.

theorem MonomialOrder.BuchbergerState.leadingCoeff_isUnit_of_ne_zero {σ : Type u_1} (m : MonomialOrder σ) {K : Type u_3} [Field K] (f : MvPolynomial σ K) (hf : f ≠ 0) : IsUnit (m.leadingCoeff f)

theorem MonomialOrder.BuchbergerState.leadingCoeff_condition_of_field {σ : Type u_1} (m : MonomialOrder σ) {K : Type u_3} [Field K] (G : Set (MvPolynomial σ K)) (g : MvPolynomial σ K) : g ∈ G → IsUnit (m.leadingCoeff g) ∨ g = 0

theorem MonomialOrder.BuchbergerState.exists_isGroebnerBasis_terminal_field {σ : Type u_1} (m : MonomialOrder σ) {K : Type u_3} [Field K] [IsNoetherianRing (MvPolynomial σ K)] {G : Set (MvPolynomial σ K)} {I : Ideal (MvPolynomial σ K)} (hspan : Ideal.span G = I) : ∃ (H : m.BuchbergerState), Relation.ReflTransGen (Step m) ⟨G, ⋯⟩ H ∧ Terminal m H ∧ m.IsGroebnerBasis (↑H) I

Field version of the terminal-state correctness theorem.

Over a field, every nonzero leading coefficient is a unit, so the coefficient condition in exists_isGroebnerBasis_terminal is automatic.

theorem MonomialOrder.BuchbergerState.exists_isGroebnerBasis_terminal_field_of_finite_variables {σ : Type u_1} (m : MonomialOrder σ) {K : Type u_3} [Field K] [IsNoetherianRing K] [Finite σ] {G : Set (MvPolynomial σ K)} {I : Ideal (MvPolynomial σ K)} (hspan : Ideal.span G = I) : ∃ (H : m.BuchbergerState), Relation.ReflTransGen (Step m) ⟨G, ⋯⟩ H ∧ Terminal m H ∧ m.IsGroebnerBasis (↑H) I

Finite-variable field version of the abstract Buchberger procedure.

If the coefficient field is Noetherian and the variable type is finite, the Noetherian hypothesis on MvPolynomial σ K is provided by Hilbert's basis theorem.

theorem MonomialOrder.BuchbergerState.exists_finite_isGroebnerBasis_terminal_field_of_finite_variables {σ : Type u_1} (m : MonomialOrder σ) {K : Type u_3} [Field K] [IsNoetherianRing K] [Finite σ] {G : Set (MvPolynomial σ K)} {I : Ideal (MvPolynomial σ K)} (hG : G.Finite) (hspan : Ideal.span G = I) : ∃ (H : m.BuchbergerState), Relation.ReflTransGen (Step m) ⟨G, ⋯⟩ H ∧ Terminal m H ∧ (↑H).Finite ∧ m.IsGroebnerBasis (↑H) I

Finite-output version of the terminal-state correctness theorem over a field with finitely many variables.

Starting from a finite polynomial set, the abstract procedure reaches a finite terminal set that is a Gröbner basis of the ideal generated by the initial set.