Polynomial reductions

This file defines one-step polynomial reduction with respect to a monomial order and a set of multivariate polynomials. It proves termination of reduction using the colexicographic order on supports, basic translation lemmas, and local confluence results for singleton reductions.

References

• [Becker and Weispfenning, Gröbner bases][Becker-Weispfenning1993]

theorem Finset.Colex.wellFounded {α : Type u_2} [LinearOrder α] [WellFoundedLT α] : WellFounded fun (x1 x2 : Colex (Finset α)) => x1 < x2

The colexicographic order on finite subsets of a well-ordered type is well-founded.

def MonomialOrder.ReducesToBy {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (p f g : MvPolynomial σ R) (t : σ →₀ ℕ) : Prop

Reduction of f by a polynomial p at the term t.

This means that t occurs in f and is divisible by the leading monomial of p. More precisely, there is a monomial s such that s + m.degree p = t, and a coefficient c such that the leading term of monomial s c * p has the same coefficient as the term t of f.

The resulting polynomial g is obtained from f by subtracting this multiple of p, so that the term t is eliminated.

Equations

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

def MonomialOrder.ReducesToPoly {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (p f g : MvPolynomial σ R) : Prop

One-step reduction modulo a single polynomial p.

Equations

• m.ReducesToPoly p f g = ∃ (t : σ →₀ ℕ), m.ReducesToBy p f g t

def MonomialOrder.ReducesToSet {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (f g : MvPolynomial σ R) : Prop

One-step reduction modulo a set P.

Equations

• m.ReducesToSet P f g = ∃ p ∈ P, m.ReducesToPoly p f g

def MonomialOrder.Reducible {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (p f : MvPolynomial σ R) : Prop

Reducibility modulo a single polynomial.

Equations

• m.Reducible p f = ∃ (g : MvPolynomial σ R), m.ReducesToPoly p f g

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

Reducibility modulo a set.

Equations

• m.ReducibleSet P f = ∃ (g : MvPolynomial σ R), m.ReducesToSet P f g

def MonomialOrder.LTermReducesToPoly {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (p f g : MvPolynomial σ R) : Prop

One-step reduction of the leading term of f modulo a single polynomial p.

Equations

• m.LTermReducesToPoly p f g = m.ReducesToBy p f g (m.degree f)

def Reduction.«term_⟶[_,_]_» : Lean.TrailingParserDescr

One-step reduction modulo a set P.

The notation f ⟶[m, P] g means that f reduces to g in one step modulo the set of polynomials P, with respect to the monomial order m.

Equations

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

def Reduction.«term_⟶*[_,_]_» : Lean.TrailingParserDescr

Finite reduction modulo a set P.

This is the reflexive-transitive closure of one-step reduction modulo P.

Equations

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

def Reduction.«term_⟷[_,_]_» : Lean.TrailingParserDescr

Symmetric one-step reduction modulo a set P.

Equations

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

def Reduction.«term_⟷*[_,_]_» : Lean.TrailingParserDescr

Equivalence closure generated by reduction modulo a set P.

Equations

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

def Reduction.«term_↓[_,_]_» : Lean.TrailingParserDescr

Joinability modulo a set P.

The notation f ↓[m, P] g means that f and g reduce to a common polynomial by finite reductions modulo P.

Equations

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

@[reducible, inline]

abbrev MonomialOrder.ReducesToPoly.NormalForm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (p f : MvPolynomial σ R) : Prop

Normal form modulo a single polynomial.

Equations

• MonomialOrder.ReducesToPoly.NormalForm m p f = Relation.IsNormalForm (m.ReducesToPoly p) f

theorem MonomialOrder.ReducesToPoly.reducible_iff_exists_degree_le_and_leadingCoeff_dvd {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (p f : MvPolynomial σ R) : m.Reducible p f ↔ p ≠ 0 ∧ ∃ t ∈ f.support, m.degree p ≤ t ∧ m.leadingCoeff p ∣ MvPolynomial.coeff t f

A polynomial is reducible modulo p exactly when p is nonzero and some support exponent t satisfies m.degree p ≤ t, while m.leadingCoeff p divides the corresponding coefficient f.coeff t.

theorem MonomialOrder.ReducesToPoly.reducible_iff_exists_degree_le_of_isUnit {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (p f : MvPolynomial σ R) (hLC : IsUnit (m.leadingCoeff p)) : m.Reducible p f ↔ p ≠ 0 ∧ ∃ t ∈ f.support, m.degree p ≤ t

Lemma 5.20(i), unit-leading-coefficient version.

If the leading coefficient of p is a unit, then reducibility modulo p is equivalent to divisibility of some term of f by the leading monomial of p.

@[reducible, inline]

abbrev MonomialOrder.ReducesToSet.ReflTransGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) : MvPolynomial σ R → MvPolynomial σ R → Prop

Reflexive-transitive closure of one-step reduction modulo P.

Equations

• MonomialOrder.ReducesToSet.ReflTransGen m P f g = Relation.ReflTransGen (m.ReducesToSet P) f g

@[reducible, inline]

abbrev MonomialOrder.ReducesToSet.EqvGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) : MvPolynomial σ R → MvPolynomial σ R → Prop

Equivalence closure generated by one-step reduction modulo P.

Equations

• MonomialOrder.ReducesToSet.EqvGen m P f g = Relation.EqvGen (m.ReducesToSet P) f g

@[reducible, inline]

abbrev MonomialOrder.ReducesToSet.Join {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) : MvPolynomial σ R → MvPolynomial σ R → Prop

Joinability modulo P.

Equations

• MonomialOrder.ReducesToSet.Join m P f g = Relation.Join (Relation.ReflTransGen (m.ReducesToSet P)) f g

@[reducible, inline]

abbrev MonomialOrder.ReducesToSet.NormalForm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (f : MvPolynomial σ R) : Prop

Normal form modulo a set P.

Equations

• MonomialOrder.ReducesToSet.NormalForm m P f = Relation.IsNormalForm (m.ReducesToSet P) f

theorem MonomialOrder.ReducesToSet.normalForm_iff_forall_not_degree_le_and_dvd {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f : MvPolynomial σ R} : Relation.IsNormalForm (m.ReducesToSet P) f ↔ ∀ t ∈ f.support, ∀ p ∈ P, p ≠ 0 → ¬(m.degree p ≤ t ∧ m.leadingCoeff p ∣ MvPolynomial.coeff t f)

Without assumptions on leading coefficients, a polynomial is in normal form exactly when there is no support exponent t and nonzero reducer p such that m.degree p ≤ t and m.leadingCoeff p ∣ f.coeff t.

theorem MonomialOrder.ReducesToSet.normalForm_iff_forall_not_degree_le {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (hP₀ : ∀ p ∈ P, IsUnit (m.leadingCoeff p) ∨ p = 0) {f : MvPolynomial σ R} : Relation.IsNormalForm (m.ReducesToSet P) f ↔ ∀ t ∈ f.support, ∀ p ∈ P, p ≠ 0 → ¬m.degree p ≤ t

If every nonzero reducer has unit leading coefficient, normal forms are exactly the polynomials whose support terms are not divisible by the leading monomial of any nonzero reducer.

This is the unit-leading-coefficient specialization of normalForm_iff_forall_not_degree_le_and_dvd.

def MonomialOrder.supportColexLt {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) : Prop

The strict order on polynomials induced from the colex order on finite supports.

The support of a polynomial is transported to the synonym type m.syn using the monomial order equivalence m.toSyn, and then compared by the colex order on finite subsets.

Equations

• m.supportColexLt f g = (toColex (Finset.image (⇑m.toSyn) f.support) < toColex (Finset.image (⇑m.toSyn) g.support))

theorem MonomialOrder.supportColexLt_wellFounded {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] : WellFounded m.supportColexLt

The support-colex order on polynomials is well-founded.

theorem MonomialOrder.ReducesToPoly.coeff_eq_zero_of_reducesToBy {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p f g : MvPolynomial σ R} {t s : σ →₀ ℕ} {c : R} (_hp : p ≠ 0) (_ht : t ∈ f.support) (hs : s + m.degree p = t) (hc : c * m.leadingCoeff p = MvPolynomial.coeff t f) (hg : g = f - (MvPolynomial.monomial s) c * p) : MvPolynomial.coeff t g = 0

In a one-step reduction eliminating the term t, the coefficient of t in the reduced polynomial is zero.

theorem MonomialOrder.ReducesToPoly.coeff_eq_of_reduced_term_lt {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p f g : MvPolynomial σ R} {t s d : σ →₀ ℕ} {c : R} (_hp : p ≠ 0) (hs : s + m.degree p = t) (hg : g = f - (MvPolynomial.monomial s) c * p) (hd : m.toSyn t < m.toSyn d) : MvPolynomial.coeff d g = MvPolynomial.coeff d f

If d is strictly larger than the term t being reduced, then its coefficient is unchanged by the one-step reduction.

theorem MonomialOrder.ReducesToPoly.supportColexLt {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p f g : MvPolynomial σ R} (h : m.ReducesToPoly p f g) : m.supportColexLt g f

Lemma 5.20(iv), single-polynomial form.

Every one-step reduction modulo a single polynomial strictly decreases the support-colex order.

theorem MonomialOrder.ReducesToSet.supportColexLt {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : m.ReducesToSet P f g) : m.supportColexLt g f

theorem MonomialOrder.ReducesToSet.wellFounded {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) : WellFounded (flip (m.ReducesToSet P))

theorem MonomialOrder.ReducesToSet.asymm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) : Std.Asymm (m.ReducesToSet P)

theorem MonomialOrder.monomial_mul_reducesToPoly {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (u : σ →₀ ℕ) {p f g : MvPolynomial σ R} (h : m.ReducesToPoly p f g) : m.ReducesToPoly p ((MvPolynomial.monomial u) 1 * f) ((MvPolynomial.monomial u) 1 * g)

Lemma 5.24(ii), single-polynomial version.

If f reduces to g modulo a single polynomial p, then multiplying both sides by a monomial preserves the one-step reduction.

theorem MonomialOrder.subLTerm_eq_zero_of_degree_eq_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {h : MvPolynomial σ R} (hdeg : m.degree h = 0) : m.subLTerm h = 0

If a polynomial has degree zero, then deleting its leading term gives zero.

theorem MonomialOrder.mul_mem_reducesTo_subLTerm_mul {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f h : MvPolynomial σ R} (hfP : f ∈ P) (hLCf : m.leadingCoeff f ∈ nonZeroDivisors R) (hh : h ≠ 0) : m.ReducesToSet P (h * f) (m.subLTerm h * f)

A product h * f reduces in one step to (m.subLTerm h) * f modulo P, provided f ∈ P, h ≠ 0, and the leading coefficient of f is a non-zero-divisor.

theorem MonomialOrder.mul_mem_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f h : MvPolynomial σ R} (hfP : f ∈ P) (hLCf : f ≠ 0 → m.leadingCoeff f ∈ nonZeroDivisors R) : Relation.ReflTransGen (m.ReducesToSet P) (h * f) 0

Lemma 5.24(i), regular-leading-coefficient version.

If f ∈ P and the leading coefficient of f is a non-zero-divisor whenever f is nonzero, then every polynomial multiple of f reduces to zero modulo P.

theorem MonomialOrder.translation_reflTransGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (hP₀ : ∀ p ∈ P, IsUnit (m.leadingCoeff p) ∨ p = 0) (f g h h₁ : MvPolynomial σ R) (hfgh : f - g = h) (hh₁ : Relation.ReflTransGen (m.ReducesToSet P) h h₁) : ∃ (f₁ : MvPolynomial σ R) (g₁ : MvPolynomial σ R), f₁ - g₁ = h₁ ∧ Relation.ReflTransGen (m.ReducesToSet P) f f₁ ∧ Relation.ReflTransGen (m.ReducesToSet P) g g₁

Translation Lemma, part (i).

theorem MonomialOrder.join_of_sub_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (hP₀ : ∀ p ∈ P, IsUnit (m.leadingCoeff p) ∨ p = 0) (f g : MvPolynomial σ R) (hfg : Relation.ReflTransGen (m.ReducesToSet P) (f - g) 0) : Relation.Join (Relation.ReflTransGen (m.ReducesToSet P)) f g

Translation Lemma, part (ii): joinability.

theorem MonomialOrder.eqvGen_of_sub_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (hP₀ : ∀ p ∈ P, IsUnit (m.leadingCoeff p) ∨ p = 0) (f g : MvPolynomial σ R) (hfg : Relation.ReflTransGen (m.ReducesToSet P) (f - g) 0) : Relation.EqvGen (m.ReducesToSet P) f g

Translation Lemma, part (ii): equivalence closure.

theorem MonomialOrder.degree_le_of_reducesToSet {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (B : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : m.ReducesToSet B f g) : m.toSyn (m.degree g) ≤ m.toSyn (m.degree f)

One-step reduction does not increase degree.

theorem MonomialOrder.degree_le_of_reflTransGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (B : Set (MvPolynomial σ R)) {f r : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet B) f r) : m.toSyn (m.degree r) ≤ m.toSyn (m.degree f)

Finite reduction does not increase degree.

theorem MonomialOrder.exists_linearCombination_of_reducesToSet {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (B : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : m.ReducesToSet B f g) : ∃ (q : ↑B →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) q + g

One-step reduction gives an explicit one-term quotient representation.

This is the first bridge from the relation-theoretic reduction API to the remainder-style statement used by the division theorem: if f reduces to g modulo B, then f is a finite linear combination of elements of B, plus g.

theorem MonomialOrder.exists_linearCombination_of_reducesToSet_with_degree_bound {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (B : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : m.ReducesToSet B f g) : ∃ (q : ↑B →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) q + g ∧ ∀ (b : ↑B), m.toSyn (m.degree (↑b * q b)) ≤ m.toSyn (m.degree f)

One-step reduction gives a quotient representation satisfying the product degree bound used by MonomialOrder.div_set.

theorem MonomialOrder.exists_linearCombination_of_reflTransGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (B : Set (MvPolynomial σ R)) {f r : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet B) f r) : ∃ (q : ↑B →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) q + r

Finite reduction gives an explicit quotient representation.

If f ⟶*[m, B] r, then f is a finite linear combination of elements of B, plus the final reduct r.

theorem MonomialOrder.exists_linearCombination_of_reflTransGen_with_degree_bound {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (B : Set (MvPolynomial σ R)) {f r : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet B) f r) : ∃ (q : ↑B →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) q + r ∧ ∀ (b : ↑B), m.toSyn (m.degree (↑b * q b)) ≤ m.toSyn (m.degree f)

Finite reduction gives a quotient representation satisfying the product degree bound used by MonomialOrder.div_set.

theorem MonomialOrder.sub_mem_span_of_reducesToSet {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : m.ReducesToSet P f g) : f - g ∈ Ideal.span P

If f reduces to g in one step modulo P, then f - g belongs to the ideal generated by P.

theorem MonomialOrder.sub_mem_span_of_reflTransGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet P) f g) : f - g ∈ Ideal.span P

theorem MonomialOrder.sub_mem_span_of_eqvGen {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f g : MvPolynomial σ R} (h : Relation.EqvGen (m.ReducesToSet P) f g) : f - g ∈ Ideal.span P

theorem MonomialOrder.mem_span_of_reflTransGen_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) {f : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet P) f 0) : f ∈ Ideal.span P

theorem MonomialOrder.eqvGen_add_mul_mem {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (hP₀ : ∀ p ∈ P, IsUnit (m.leadingCoeff p) ∨ p = 0) {f h p : MvPolynomial σ R} (hpP : p ∈ P) : Relation.EqvGen (m.ReducesToSet P) (f + h * p) f

A polynomial multiple of an element of P can be removed up to the equivalence closure generated by reduction modulo P.

theorem MonomialOrder.eqvGen_iff_sub_mem_span {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (hP₀ : ∀ p ∈ P, IsUnit (m.leadingCoeff p) ∨ p = 0) {f g : MvPolynomial σ R} : Relation.EqvGen (m.ReducesToSet P) f g ↔ f - g ∈ Ideal.span P

Lemma 5.26.

Two polynomials are equivalent modulo the ideal generated by P iff they are equivalent under the equivalence closure of reduction modulo P.

theorem MonomialOrder.ReducesToSet.singleton_iff {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p f g : MvPolynomial σ R} : m.ReducesToSet {p} f g ↔ m.ReducesToPoly p f g

theorem MonomialOrder.ReducesToSet.reflTransGen_singleton_to_reducesToPoly {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p f g : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet {p}) f g) : Relation.ReflTransGen (m.ReducesToPoly p) f g

Finite reduction modulo the singleton set {p} gives finite reduction modulo the single polynomial p.

theorem MonomialOrder.ReducesToSet.reflTransGen_reducesToPoly_to_singleton {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p f g : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToPoly p) f g) : Relation.ReflTransGen (m.ReducesToSet {p}) f g

Finite reduction modulo the single polynomial p gives finite reduction modulo the singleton set {p}.

theorem MonomialOrder.ReducesToSet.reflTransGen_mono {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {P Q : Set (MvPolynomial σ R)} (hQP : Q ⊆ P) {f g : MvPolynomial σ R} (h : Relation.ReflTransGen (m.ReducesToSet Q) f g) : Relation.ReflTransGen (m.ReducesToSet P) f g

If Q ⊆ P, then finite reductions modulo Q are finite reductions modulo P.

theorem MonomialOrder.ReducesToSet.locallyConfluent_singleton {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p : MvPolynomial σ R} (hpLC : IsUnit (m.leadingCoeff p)) : Relation.LocallyConfluent (m.ReducesToSet {p})

Proposition 5.33, singleton-set version.

If p has unit leading coefficient, then reduction modulo {p} is locally confluent.

theorem MonomialOrder.ReducesToPoly.locallyConfluent {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {p : MvPolynomial σ R} (hpLC : IsUnit (m.leadingCoeff p)) : Relation.LocallyConfluent (m.ReducesToPoly p)

Proposition 5.33.

If p has unit leading coefficient, then reduction modulo the single polynomial p is locally confluent.

theorem MonomialOrder.ReducesToSet.locallyConfluent_of_span_eq_singleton {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (P : Set (MvPolynomial σ R)) (hP₀ : ∀ q ∈ P, IsUnit (m.leadingCoeff q) ∨ q = 0) {p : MvPolynomial σ R} (hpP : p ∈ P) (hp : p ≠ 0) (hspan : Ideal.span P = Ideal.span {p}) : Relation.LocallyConfluent (m.ReducesToSet P)

Corollary 5.34.

If Ideal.span P = Ideal.span {p} for some nonzero p ∈ P, and all nonzero elements of P have unit leading coefficient, then reduction modulo P is locally confluent.