Gröbner basis criterion

This file formalizes the Gröbner basis criterion in the setting of Becker--Weispfenning--Kredel, Theorem 5.35.

We take the leading-term criterion for a subset G itself as the definition:

• a set G satisfies IsGroebner if the ideal generated by the leading terms of all elements of ⟨G⟩ is equal to the ideal generated by the leading terms of elements of G.

The file then relates this definition to the reduction-theoretic properties appearing in Theorem 5.35:

• local confluence of reduction modulo G;
• confluence of reduction modulo G;
• uniqueness of normal forms;
• the Church--Rosser property;
• reduction to zero for all elements of ⟨G⟩;
• reducibility of all nonzero elements of ⟨G⟩;
• uniqueness of normal-form representatives modulo ⟨G⟩.

The main implication cycle follows the proof of Theorem 5.35:

• IsGroebner G implies uniqueness of normal-form representatives modulo ⟨G⟩;
• uniqueness of normal-form representatives implies the Church--Rosser property;
• the Church--Rosser property is equivalent to reduction to zero for all elements of ⟨G⟩;
• reduction to zero for all elements of ⟨G⟩ implies reducibility of all nonzero elements of ⟨G⟩;
• reducibility of all nonzero elements of ⟨G⟩ implies IsGroebner G.

After this cycle is established, the resulting equivalences are recorded as separate theorem statements for later use.

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

IsGroebner G means that G satisfies the leading-term criterion for the ideal it generates: the ideal generated by the leading terms of elements of Ideal.span G is generated by the leading terms of elements of G.

Equations

• m.IsGroebner G = (Ideal.span (m.leadingTerm '' ↑(Ideal.span G)) = Ideal.span (m.leadingTerm '' G))

theorem MonomialOrder.IsGroebner.zero_isNormalForm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) : Relation.IsNormalForm (m.ReducesToSet G) 0

The zero polynomial is in normal form with respect to reduction modulo G.

theorem MonomialOrder.IsGroebner.churchRosser_iff_idealElements_reduceTo_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) : Relation.ChurchRosser (m.ReducesToSet G) ↔ ∀ f ∈ Ideal.span G, Relation.ReflTransGen (m.ReducesToSet G) f 0

The Church--Rosser property is equivalent to the statement that every element of Ideal.span G reduces to zero modulo G.

This is one of the reduction-theoretic formulations of the Gröbner basis criterion.

theorem MonomialOrder.IsGroebner.idealElements_reduceTo_zero_imp_nonzero_idealElements_reducible {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) : (∀ f ∈ Ideal.span G, Relation.ReflTransGen (m.ReducesToSet G) f 0) → ∀ (f : MvPolynomial σ R), f ≠ 0 → f ∈ Ideal.span G → m.ReducibleSet G f

If every element of Ideal.span G reduces to zero modulo G, then every nonzero element of Ideal.span G is reducible modulo G.

theorem MonomialOrder.IsGroebner.nonzero_idealElements_reducible_imp_isGroebner {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) : (∀ (f : MvPolynomial σ R), f ≠ 0 → f ∈ Ideal.span G → m.ReducibleSet G f) → m.IsGroebner G

If every nonzero element of Ideal.span G is reducible modulo G, then G satisfies the Gröbner criterion.

theorem MonomialOrder.IsGroebner.isGroebner_imp_unique_normalForm_representatives {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : m.IsGroebner G → ∀ (f : MvPolynomial σ R), ∃! n : MvPolynomial σ R, Relation.IsNormalForm (m.ReducesToSet G) n ∧ f - n ∈ Ideal.span G

If G satisfies the Gröbner criterion, then every congruence class modulo Ideal.span G has a unique representative in normal form.

theorem MonomialOrder.IsGroebner.unique_normalForm_representatives_imp_churchRosser {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) : (∀ (f : MvPolynomial σ R), ∃! n : MvPolynomial σ R, Relation.IsNormalForm (m.ReducesToSet G) n ∧ f - n ∈ Ideal.span G) → Relation.ChurchRosser (m.ReducesToSet G)

Uniqueness of normal-form representatives modulo Ideal.span G implies the Church--Rosser property.

theorem MonomialOrder.IsGroebner.iff_idealElements_reduceTo_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) : m.IsGroebner G ↔ ∀ f ∈ Ideal.span G, Relation.ReflTransGen (m.ReducesToSet G) f 0

A set G satisfies the Gröbner criterion iff every element of Ideal.span G reduces to zero modulo G.

theorem MonomialOrder.IsGroebner.iff_nonzero_idealElements_reducible {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : m.IsGroebner G ↔ ∀ (f : MvPolynomial σ R), f ≠ 0 → f ∈ Ideal.span G → m.ReducibleSet G f

The Gröbner criterion is equivalent to reducibility of every nonzero element of Ideal.span G.

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

The Gröbner criterion is equivalent to the Church--Rosser property.

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

The Gröbner criterion is equivalent to local confluence of reduction modulo G.

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

The Gröbner criterion is equivalent to confluence of reduction modulo G.

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

The Gröbner criterion is equivalent to uniqueness of normal forms.

theorem MonomialOrder.IsGroebner.iff_unique_normalForm_representatives {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (G : Set (MvPolynomial σ R)) (hG₀ : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) : m.IsGroebner G ↔ ∀ (f : MvPolynomial σ R), ∃! n : MvPolynomial σ R, Relation.IsNormalForm (m.ReducesToSet G) n ∧ f - n ∈ Ideal.span G

The Gröbner criterion is equivalent to uniqueness of normal-form representatives modulo Ideal.span G.