Orderings on polynomials and triangular sets

This file defines order structures on multivariate polynomials and triangular sets, which are essential for the Characteristic Set Method (Wu's Method).

Main definitions

• MvPolynomial.order: The order of a polynomial p is the pair (max_vars p, mainDegree p), ordered lexicographically. This defines a well-ordering on polynomials when the variable type is well-founded.

• TriangularSet.order: The order of a triangular set is a lexicographic sequence of orders of its polynomials. For two triangular sets S and T, S < T if either:

  1. There exists k < S.length such that S₀ ≈ T₀, S₁ ≈ T₁, ..., Sₖ₋₁ ≈ Tₖ₋₁ and Sₖ < Tₖ;
  2. S.length > T.length and ∀ i < T.length, Sᵢ ≈ Tᵢ.

Main results

• MvPolynomial.instWellFoundedLT: When σ is well-founded, polynomials are well-founded under the order ordering.

• TriangularSet.instWellFoundedLT: When σ is finite, triangular sets are well-founded under the order ordering. This guarantees termination of characteristic set algorithms.

noncomputable def MvPolynomial.order {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) : Lex (WithBot σ × ℕ)

The order of a polynomial p is the pair (max_vars p, degree p), which is ordered lexicographically.

Equations

• p.order = (p.vars.max, p.mainDegree)

theorem MvPolynomial.order_eq_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p.order = q.order ↔ p.vars.max = q.vars.max ∧ p.mainDegree = q.mainDegree

@[implicit_reducible]

instance MvPolynomial.instPreorder {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Preorder (MvPolynomial σ R)

Equations

• MvPolynomial.instPreorder = { le := InvImage (fun (x1 x2 : Lex (WithBot σ × ℕ)) => x1 ≤ x2) MvPolynomial.order, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem MvPolynomial.le_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ p.order ≤ q.order

@[implicit_reducible]

noncomputable instance MvPolynomial.instDecidableLE {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLE (MvPolynomial σ R)

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹.order ≤ x✝.order) ⋯

@[implicit_reducible]

noncomputable instance MvPolynomial.instDecidableLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLT (MvPolynomial σ R)

Equations

• MvPolynomial.instDecidableLT = decidableLTOfDecidableLE

instance MvPolynomial.instIsTotalLe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Std.Total LE.le

theorem MvPolynomial.le_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ p.vars.max < q.vars.max ∨ p.vars.max = q.vars.max ∧ p.mainDegree ≤ q.mainDegree

theorem MvPolynomial.le_iff_not_imp {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ ¬p.vars.max < q.vars.max → p.vars.max = q.vars.max ∧ p.mainDegree ≤ q.mainDegree

theorem MvPolynomial.max_vars_le_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q → p.vars.max ≤ q.vars.max

theorem MvPolynomial.lt_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p < q ↔ p.order < q.order

theorem MvPolynomial.lt_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p < q ↔ p.vars.max < q.vars.max ∨ p.vars.max = q.vars.max ∧ p.mainDegree < q.mainDegree

theorem MvPolynomial.lt_iff_not_imp {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p < q ↔ ¬p.vars.max < q.vars.max → p.vars.max = q.vars.max ∧ p.mainDegree < q.mainDegree

theorem MvPolynomial.lt_of_max_vars_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p.vars.max < q.vars.max → p < q

@[simp]

theorem MvPolynomial.not_lt_iff_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : ¬p < q ↔ q ≤ p

@[simp]

theorem MvPolynomial.not_le_iff_gt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : ¬p ≤ q ↔ q < p

theorem MvPolynomial.X_lt_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] {i j : σ} : i < j → X i < X j

@[implicit_reducible]

instance MvPolynomial.instSetoid {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Setoid (MvPolynomial σ R)

Equations

• MvPolynomial.instSetoid = AntisymmRel.setoid (MvPolynomial σ R) fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2

@[implicit_reducible]

noncomputable instance MvPolynomial.instDecidableRelEquiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableRel fun (x1 x2 : MvPolynomial σ R) => x1 ≈ x2

Equations

• x✝¹.instDecidableRelEquiv x✝ = instDecidableAnd

theorem MvPolynomial.equiv_def'' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ p ≤ q ∧ q ≤ p

theorem MvPolynomial.equiv_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ p.order = q.order

theorem MvPolynomial.equiv_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ ¬p < q ∧ ¬q < p

theorem MvPolynomial.equiv_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ p.vars.max = q.vars.max ∧ p.mainDegree = q.mainDegree

theorem MvPolynomial.le_iff_lt_or_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ p < q ∨ p ≈ q

theorem MvPolynomial.lt_of_equiv_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q r : MvPolynomial σ R} : p ≈ q → q < r → p < r

theorem MvPolynomial.lt_of_lt_of_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q r : MvPolynomial σ R} : p < q → q ≈ r → p < r

theorem MvPolynomial.equiv_of_le_of_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q → q ≤ p → p ≈ q

theorem MvPolynomial.zero_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} : 0 ≤ p

theorem MvPolynomial.wellFoundedLT_variables_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (MvPolynomial σ R) → WellFoundedLT σ

instance MvPolynomial.instWellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT σ] : WellFoundedLT (MvPolynomial σ R)

theorem MvPolynomial.wellFoundedLT_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (MvPolynomial σ R) ↔ WellFoundedLT σ

theorem MvPolynomial.Set.has_min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) : ∃ p ∈ PS, ∀ q ∈ PS, ¬q < p

noncomputable def MvPolynomial.Set.min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) : MvPolynomial σ R

The minimal element of a nonempty set of multivariate polynomials.

Equations

• MvPolynomial.Set.min PS h = ⋯.choose

theorem MvPolynomial.Set.min_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) : min PS h ∈ PS

theorem TriangularSet.apply_lt_of_index_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} (h : n < S.length) : m < n → S m < S n

theorem TriangularSet.index_lt_of_apply_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} (h : m < S.length) : S m < S n → m < n

theorem TriangularSet.le_of_index_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} : m ≤ n → n < S.length → S m ≤ S n

Order and Ordering

noncomputable def TriangularSet.order {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) : Lex (ℕ → WithTop (Lex (WithBot σ × ℕ)))

The order of a Triangular Set is a lexicographic sequence of orders of its polynomials. A more intuitive definition is order_lt_iff, S < T if one of the following two occurs:

1. There exists some k < S.length such that S₀ ≈ T₀, S₁ ≈ T₁, ..., Sₖ₋₁ ≈ Tₖ₋₁ and Sₖ < Tₖ.
2. S.length > T.length and ∀ i < T.length, Sᵢ ≈ Tᵢ

Equations

• S.order i = if i < S.length then ↑(S i).order else ⊤

theorem TriangularSet.order_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} : S.order = fun (i : ℕ) => if i < S.length then ↑(S i).order else ⊤

theorem TriangularSet.order_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {i : ℕ} (h : i < S.length) : S.order i = ↑(S i).order

theorem TriangularSet.order_apply' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {i : ℕ} (h : S.length ≤ i) : S.order i = ⊤

theorem TriangularSet.order_lt_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S.order < T.order ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length < S.length ∧ ∀ i < T.length, S i ≈ T i

theorem TriangularSet.order_eq_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S.order = T.order ↔ S.length = T.length ∧ ∀ (k : ℕ), S k ≈ T k

theorem TriangularSet.order_le_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S.order ≤ T.order ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length ≤ S.length ∧ ∀ k < T.length, S k ≤ T k

@[implicit_reducible]

instance TriangularSet.instPreorder {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Preorder (TriangularSet σ R)

Equations

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

theorem TriangularSet.le_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T ↔ S.order ≤ T.order

@[implicit_reducible]

noncomputable instance TriangularSet.instDecidableLE {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLE (TriangularSet σ R)

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹.order ≤ x✝.order) ⋯

@[implicit_reducible]

noncomputable instance TriangularSet.instDecidableLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLT (TriangularSet σ R)

Equations

• TriangularSet.instDecidableLT = decidableLTOfDecidableLE

instance TriangularSet.instTotalLe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Std.Total LE.le

theorem TriangularSet.le_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length ≤ S.length ∧ ∀ k < T.length, S k ≤ T k

theorem TriangularSet.lt_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S < T ↔ S.order < T.order

theorem TriangularSet.lt_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S < T ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length < S.length ∧ ∀ i < T.length, S i ≈ T i

theorem TriangularSet.lt_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} : S ≠ ∅ → S < ∅

theorem TriangularSet.le_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) : S ≤ ∅

@[simp]

theorem TriangularSet.not_lt_iff_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : ¬S < T ↔ T ≤ S

@[simp]

theorem TriangularSet.not_le_iff_gt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : ¬S ≤ T ↔ T < S

theorem TriangularSet.ge_of_forall_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : (∀ n < S.length, ∃ i < T.length, T i ≈ S n) → T ≤ S

theorem TriangularSet.ge_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ⊆ T → T ≤ S

@[implicit_reducible]

instance TriangularSet.instSetoid {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Setoid (TriangularSet σ R)

Equations

• TriangularSet.instSetoid = AntisymmRel.setoid (TriangularSet σ R) fun (x1 x2 : TriangularSet σ R) => x1 ≤ x2

@[implicit_reducible]

noncomputable instance TriangularSet.instDecidableRelEquiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableRel fun (x1 x2 : TriangularSet σ R) => x1 ≈ x2

Equations

• x✝¹.instDecidableRelEquiv x✝ = instDecidableAnd

theorem TriangularSet.equiv_def'' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S ≤ T ∧ T ≤ S

theorem TriangularSet.equiv_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S.order = T.order

theorem TriangularSet.equiv_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ ¬S < T ∧ ¬T < S

theorem TriangularSet.equiv_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S.length = T.length ∧ ∀ (k : ℕ), S k ≈ T k

theorem TriangularSet.equiv_iff' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S.length = T.length ∧ ∀ k < S.length, S k ≈ T k

theorem TriangularSet.le_iff_lt_or_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T ↔ S < T ∨ S ≈ T

theorem TriangularSet.lt_of_equiv_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T U : TriangularSet σ R} : S ≈ T → T < U → S < U

theorem TriangularSet.lt_of_lt_of_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T U : TriangularSet σ R} : S < T → T ≈ U → S < U

theorem TriangularSet.equiv_of_le_of_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T → T ≤ S → S ≈ T

theorem TriangularSet.gt_of_ssubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ⊂ T → T < S

theorem TriangularSet.lt_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} : n < S.length → S < S.take n

theorem TriangularSet.lt_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} : S ≠ ∅ → 0 < n → S < S.drop n

theorem TriangularSet.concat_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) : S.concat p h < S

theorem TriangularSet.single_lt_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} [DecidableEq R] : p ≠ 0 → single p < ∅

theorem TriangularSet.gt_single_of_first_gt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} {S : TriangularSet σ R} [DecidableEq R] : p ≠ 0 → p < S 0 → single p < S

Well-Foundedness

theorem TriangularSet.wellFoundedLT_mvPolynomial_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : WellFoundedLT (TriangularSet σ R) → WellFoundedLT (MvPolynomial σ R)

theorem TriangularSet.wellFoundedLT_variables_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (TriangularSet σ R) → WellFoundedLT σ

theorem TriangularSet.wellFoundedGT_variables_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (TriangularSet σ R) → WellFoundedGT σ

theorem TriangularSet.length_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} [Fintype σ] : S.length ≤ Fintype.card σ + 1

instance TriangularSet.instIsWellFoundedOrderLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] : IsWellFounded (TriangularSet σ R) (InvImage (fun (x1 x2 : Lex (ℕ → WithTop (Lex (WithBot σ × ℕ)))) => x1 < x2) order)

The set of Triangular Sets is well-founded under the lexicographic order ordering. This is a crucial result that guarantees the termination of the Characteristic Set Algorithm.

instance TriangularSet.instWellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] : WellFoundedLT (TriangularSet σ R)

@[implicit_reducible]

instance TriangularSet.instWellFoundedRelation {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] : WellFoundedRelation (TriangularSet σ R)

Equations

• TriangularSet.instWellFoundedRelation = { rel := fun (x1 x2 : TriangularSet σ R) => x1 < x2, wf := ⋯ }

theorem TriangularSet.Set.has_min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) : ∃ S ∈ S', ∀ T ∈ S', S ≤ T

noncomputable def TriangularSet.Set.min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) : TriangularSet σ R

The minimal element of a nonempty set of triangular sets.

Equations

• TriangularSet.Set.min S' h = ⋯.choose

theorem TriangularSet.Set.min_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) : min S' h ∈ S'

theorem TriangularSet.Set.min_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) (T : TriangularSet σ R) : T ∈ S' → min S' h ≤ T