The Buchberger Algorithm

This file contains the formalization of the Buchberger algorithm, which computes a Gröbner basis for any ideal in a polynomial ring over a field.

The algorithm is proven correct in two distinct styles:

1. Explicit Recursion (Buchberger_Step, Buchberger_Alg): An explicit recursive function is defined, and its termination and correctness are proven using helper lemmas about its properties (invariants).
2. Well-Founded Recursion (Buchberger_Alg_wf): A more abstract approach using WellFounded.fix, which is a common and powerful pattern in mathlib. This separates the one-step logic of the algorithm from the recursion mechanism itself.

Termination for both proofs is guaranteed by Hilbert's Basis Theorem, which ensures that the strictly increasing chain of initial ideals generated at each step must eventually stabilize.

Main Definitions

• MvPolynomial.NonZero_Rem_Spoly: A helper function that computes the set of S-polynomials which do not reduce to zero with respect to the current basis.
• MvPolynomial.Buchberger_Step: A recursive function implementing one step of the explicit version of the Buchberger algorithm.

Main Results

• MvPolynomial.lt_ideal_span_of_rem_spoly_nonempty: The key lemma for the termination proof, showing that adding non-zero remainders strictly increases the initial ideal.
• MvPolynomial.Buchberger_Alg: The main theorem (first version), proving that the explicit recursive algorithm terminates and returns a valid Gröbner basis.
• MvPolynomial.Buchberger_Alg_wf: The main theorem (second version), proving the same result using well-founded recursion.

instance Field.isNoetherianRing {k : Type u_2} [Field k] : IsNoetherianRing k

def MvPolynomial.reduces_to_zero {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (G : Finset (MvPolynomial σ k)) (f : MvPolynomial σ k) : Prop

Equations

• MvPolynomial.reduces_to_zero G f = ∃ (A : MvPolynomial σ k → MvPolynomial σ k), f = ∑ g ∈ G, A g * g ∧ ∀ g ∈ G, A g * g ≠ 0 → m.toSyn (m.degree (A g * g)) ≤ m.toSyn (m.degree f)

theorem MvPolynomial.normalForm_not_divisible_by_basis {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (G : Finset (MvPolynomial σ k)) (hG : ∀ g ∈ G, g ≠ 0) (p : MvPolynomial σ k) (d : σ →₀ ℕ) (hd_in_support : d ∈ (normalForm m hG p).support) (b : MvPolynomial σ k) : b ∈ G → ¬m.degree b ≤ d

theorem MvPolynomial.leadingTerm_normalForm_not_mem_ideal_span_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] (G : Finset (MvPolynomial σ k)) (hG : ∀ g ∈ G, g ≠ 0) (p : MvPolynomial σ k) (h_rem_ne_zero : normalForm m hG p ≠ 0) : m.leadingTerm (normalForm m hG p) ∉ Ideal.span ((fun (g : MvPolynomial σ k) => m.leadingTerm g) '' ↑G)

noncomputable def MvPolynomial.NonZero_Rem_Spoly {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] (G : Finset (MvPolynomial σ k)) (hG : ∀ g ∈ G, g ≠ 0) : Finset (MvPolynomial σ k)

Equations

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

theorem MvPolynomial.lt_ideal_span_of_rem_spoly_nonempty {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] {G : Finset (MvPolynomial σ k)} (hG : ∀ g ∈ G, g ≠ 0) (h_nonempty : NonZero_Rem_Spoly m G hG ≠ ∅) : Ideal.span ((fun (g : MvPolynomial σ k) => m.leadingTerm g) '' ↑G) < Ideal.span ((fun (g : MvPolynomial σ k) => m.leadingTerm g) '' (↑G ∪ ↑(NonZero_Rem_Spoly m G hG)))

@[irreducible]

noncomputable def MvPolynomial.Buchberger_Step {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] {G : Finset (MvPolynomial σ k)} (hG : ∀ g ∈ G, g ≠ 0) [Finite σ] : Finset (MvPolynomial σ k)

Equations

• MvPolynomial.Buchberger_Step m hG = if h_Rem_empty : MvPolynomial.NonZero_Rem_Spoly m G hG = ∅ then G else have hG' := ⋯; MvPolynomial.Buchberger_Step m hG'

@[irreducible]

theorem MvPolynomial.Buchberger_Step_property {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] [Finite σ] (G : Finset (MvPolynomial σ k)) (hG : ∀ g ∈ G, g ≠ 0) : G ⊆ Buchberger_Step m hG ∧ ∀ g ∈ Buchberger_Step m hG, g ≠ 0

@[irreducible]

theorem MvPolynomial.Buchberger_Step_span_property {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] [Finite σ] {G : Finset (MvPolynomial σ k)} (hG : ∀ g ∈ G, g ≠ 0) {I : Ideal (MvPolynomial σ k)} (hspan : I = Ideal.span ↑G) : I = Ideal.span ↑(Buchberger_Step m hG)

@[irreducible]

theorem MvPolynomial.NonZero_Rem_Spoly_of_Buchberger_Step_is_empty {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] [Finite σ] {G : Finset (MvPolynomial σ k)} (hG : ∀ g ∈ G, g ≠ 0) : NonZero_Rem_Spoly m (Buchberger_Step m hG) ⋯ = ∅

theorem MvPolynomial.Buchberger_Alg {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] [Finite σ] {F : Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)} (hF : ∀ f ∈ F, f ≠ 0) (hspan : I = Ideal.span ↑F) : F ⊆ Buchberger_Step m hF ∧ IsGroebnerBasis m I (Buchberger_Step m hF)

theorem MvPolynomial.Buchberger_Alg_wf {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] [Finite σ] {F : Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)} (hF : ∀ f ∈ F, f ≠ 0) (hspan : I = Ideal.span ↑F) : ∃ (G : Finset (MvPolynomial σ k)), F ⊆ G ∧ IsGroebnerBasis m I G