Triangulated Set

This file defines the structure of a Triangulated Set of multivariate polynomials. A Triangulated Set is a finite ordered sequence of non-zero polynomials [P₁, P₂, ..., Pₘ] such that their main variables (main variables) are strictly increasing: mainVariable(P₁) < mainVariable(P₂) < ... < mainVariable(Pₘ).

Main Definitions

• TriangulatedSet: The structure definition. It bundles the length, the sequence function, and the proofs of non-zero elements and ascending main variables.
• TriangulatedSet.rank: A lexicographic rank assigned to each triangulated set, used to prove termination of algorithms (like Wu's Method).
• TriangulatedSet.toFinset / toList: Viewing the sequence as a set or list of polynomials.

Main Results

• TriangulatedSet.instWellFoundedLT: Proof that triangulated sets are well-founded under the rank ordering (assuming finite variables). This guarantees termination of characteristic set algorithms.
• TriangulatedSet.takeConcat_lt_of_reducedToSet: Appending a reduced element strictly decreases the rank, used to prove termination of basic set algorithms.

structure TriangulatedSet (σ : Type u_1) (R : Type u_2) [CommSemiring R] [LinearOrder σ] : Type (max u_1 u_2)

A Triangulated Set is a finite sequence of polynomials with strictly increasing main variables.

• length' : ℕ

  The number of polynomials in the set.

• seq : ℕ → MvPolynomial σ R

  The sequence of polynomials, indexed by ℕ.

• elements_ne_zero (n : ℕ) : n < self.length' ↔ self.seq n ≠ 0

  Elements within the length bound are non-zero.

• ascending_mainVariable (n : ℕ) : n < self.length' - 1 → (self.seq n).mainVariable < (self.seq (n + 1)).mainVariable

  The main variables of the polynomials are strictly increasing.

instance TriangulatedSet.instFunLike {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : FunLike (TriangulatedSet σ R) ℕ (MvPolynomial σ R)

Equations

• TriangulatedSet.instFunLike = { coe := fun (S : TriangulatedSet σ R) => S.seq, coe_injective' := ⋯ }

def TriangulatedSet.length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : ℕ

The length of the triangulated set.

Equations

• S.length = S.length'

theorem TriangulatedSet.ext {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} (h : ∀ (i : ℕ), S i = T i) : S = T

theorem TriangulatedSet.ext_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S = T ↔ ∀ (i : ℕ), S i = T i

theorem TriangulatedSet.elements_ne_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : n < S.length ↔ S n ≠ 0

theorem TriangulatedSet.elements_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : S.length ≤ n ↔ S n = 0

theorem TriangulatedSet.ext' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} (h1 : S.length = T.length) (h2 : ∀ i < S.length, S i = T i) : S = T

@[simp]

theorem TriangulatedSet.apply_length_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : S S.length = 0

theorem TriangulatedSet.mainVariable_lt_mainVariable_next {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : n < S.length - 1 → (S n).mainVariable < (S (n + 1)).mainVariable

theorem TriangulatedSet.mainVariable_lt_mainVariable_next' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : n + 1 < S.length → (S n).mainVariable < (S (n + 1)).mainVariable

theorem TriangulatedSet.mainVariable_lt_mainVariable_next'' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : 0 < n → n < S.length → (S (n - 1)).mainVariable < (S n).mainVariable

theorem TriangulatedSet.mainVariable_lt_of_index_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {m n : ℕ} : m < n → n < S.length → (S m).mainVariable < (S n).mainVariable

theorem TriangulatedSet.false_of_mainVariable_ge_of_index_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {m n : ℕ} : m < n → n < S.length → (S n).mainVariable ≤ (S m).mainVariable → False

theorem TriangulatedSet.mainVariable_le_of_index_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {m n : ℕ} : m ≤ n → n < S.length → (S m).mainVariable ≤ (S n).mainVariable

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

theorem TriangulatedSet.index_eq_of_mainVariable_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {m n : ℕ} : m < S.length → n < S.length → (S m).mainVariable = (S n).mainVariable → m = n

theorem TriangulatedSet.index_eq_of_apply_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {m n : ℕ} : m < S.length → n < S.length → S m = S n → m = n

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

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

theorem TriangulatedSet.index_eq_zero_of_mainVariable_eq_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : n < S.length → (S n).mainVariable = ⊥ → n = 0

theorem TriangulatedSet.exists_index_mainVar_between_of_mainVar_first_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : (S 0).mainVariable < p.mainVariable) : ∃ k ≤ S.length, (S (k - 1)).mainVariable < p.mainVariable ∧ (p.mainVariable ≤ (S k).mainVariable ∨ k = S.length)

Set-like behavior

instance TriangulatedSet.instSetLike {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : SetLike (TriangulatedSet σ R) (MvPolynomial σ R)

Equations

• TriangulatedSet.instSetLike = { coe := fun (S : TriangulatedSet σ R) => {p : MvPolynomial σ R | ∃ n < S.length, S n = p}, coe_injective' := ⋯ }

theorem TriangulatedSet.mem_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} : p ∈ S ↔ ∃ n < S.length, S n = p

@[simp]

theorem TriangulatedSet.zero_notMem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : 0 ∉ S

theorem TriangulatedSet.ne_zero_of_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} : p ∈ S → p ≠ 0

theorem TriangulatedSet.apply_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : n < S.length → S n ∈ S

theorem TriangulatedSet.forall_mem_iff_forall_index {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {a : MvPolynomial σ R → Prop} : (∀ p ∈ S, a p) ↔ ∀ i < S.length, a (S i)

theorem TriangulatedSet.forall_mem_iff_forall_index' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {a : MvPolynomial σ R → Prop} {n : ℕ} (h : n = S.length) : (∀ p ∈ S, a p) ↔ ∀ (i : Fin n), a (S ↑i)

theorem TriangulatedSet.exists_mem_iff_exists_index {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {a : MvPolynomial σ R → Prop} : (∃ p ∈ S, a p) ↔ ∃ i < S.length, a (S i)

theorem TriangulatedSet.exists_mem_iff_exists_index' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {a : MvPolynomial σ R → Prop} {n : ℕ} (h : n = S.length) : (∃ p ∈ S, a p) ↔ ∃ (i : Fin n), a (S ↑i)

instance TriangulatedSet.instHasSubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : HasSubset (TriangulatedSet σ R)

Equations

• TriangulatedSet.instHasSubset = { Subset := fun (S T : TriangulatedSet σ R) => ∀ ⦃x : MvPolynomial σ R⦄, x ∈ S → x ∈ T }

instance TriangulatedSet.instHasSSubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : HasSSubset (TriangulatedSet σ R)

Equations

• TriangulatedSet.instHasSSubset = { SSubset := fun (S T : TriangulatedSet σ R) => S ⊆ T ∧ ¬T ⊆ S }

@[simp]

theorem TriangulatedSet.Subset.refl {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : S ⊆ S

theorem TriangulatedSet.Subset.trans {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T U : TriangulatedSet σ R} : S ⊆ T → T ⊆ U → S ⊆ U

theorem TriangulatedSet.subset_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S ⊆ T ↔ ∀ ⦃x : MvPolynomial σ R⦄, x ∈ S → x ∈ T

theorem TriangulatedSet.mem_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} (p : MvPolynomial σ R) (h : S ⊆ T) : p ∈ S → p ∈ T

theorem TriangulatedSet.ssubset_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S ⊂ T ↔ S ⊆ T ∧ ¬T ⊆ S

def TriangulatedSet.toFinset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : Finset (MvPolynomial σ R)

Equations

• S.toFinset = Finset.map { toFun := fun (i : Fin S.length) => S ↑i, inj' := ⋯ } Finset.univ

@[simp]

theorem TriangulatedSet.card_toFinset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : S.toFinset.card = S.length

@[simp]

theorem TriangulatedSet.mem_toFinset_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} : p ∈ S.toFinset ↔ p ∈ S

@[simp]

theorem TriangulatedSet.toFinset_eq_iff_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S.toFinset = T.toFinset ↔ S = T

theorem TriangulatedSet.toFinset_eq_coe_set {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : ↑S.toFinset = ↑S

theorem TriangulatedSet.length_le_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S ⊆ T → S.length ≤ T.length

theorem TriangulatedSet.length_lt_of_ssubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S ⊂ T → S.length < T.length

def TriangulatedSet.toList {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : List (MvPolynomial σ R)

Equations

• S.toList = List.ofFn fun (i : Fin S.length) => S ↑i

@[simp]

theorem TriangulatedSet.length_toList {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : S.toList.length = S.length

@[simp]

theorem TriangulatedSet.mem_toList_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} : p ∈ S.toList ↔ p ∈ S

@[simp]

theorem TriangulatedSet.toList_eq_iff_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S.toList = T.toList ↔ S = T

theorem TriangulatedSet.toList_getElem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} (h : n < S.toList.length) : S.toList[n] = S n

theorem TriangulatedSet.toList_non_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} ⦃p : MvPolynomial σ R⦄ : p ∈ S.toList → p ≠ 0

theorem TriangulatedSet.toList_pairwise {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) S.toList

instance TriangulatedSet.instDecidableEqOfMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq (MvPolynomial σ R)] : DecidableEq (TriangulatedSet σ R)

Equations

• x✝¹.instDecidableEqOfMvPolynomial x✝ = decidable_of_iff (x✝¹.toList = x✝.toList) ⋯

noncomputable instance TriangulatedSet.instEmptyCollection {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : EmptyCollection (TriangulatedSet σ R)

Equations

• TriangulatedSet.instEmptyCollection = { emptyCollection := TriangulatedSet.empty✝ }

noncomputable instance TriangulatedSet.instInhabited {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Inhabited (TriangulatedSet σ R)

Equations

• TriangulatedSet.instInhabited = { default := ∅ }

theorem TriangulatedSet.empty_eq_default {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : ∅ = default

@[simp]

theorem TriangulatedSet.length_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : ∅.length = 0

@[simp]

theorem TriangulatedSet.empty_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {n : ℕ} : ∅ n = 0

theorem TriangulatedSet.length_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : S.length = 0 ↔ S = ∅

theorem TriangulatedSet.length_gt_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : 0 < S.length ↔ S ≠ ∅

theorem TriangulatedSet.length_ge_one_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : 1 ≤ S.length ↔ S ≠ ∅

theorem TriangulatedSet.notMem_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) : p ∉ ∅

theorem TriangulatedSet.eq_empty_of_forall_notMem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : (∀ (p : MvPolynomial σ R), p ∉ S) → S = ∅

Rank and Ordering

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

The rank of a Triangulated Set is a lexicographic sequence of ranks of its polynomials. A more intuitive definition is rank_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.rank i = if i < S.length then ↑(S i).rank else ⊤

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

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

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

theorem TriangulatedSet.rank_lt_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S.rank < T.rank ↔ (∃ 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 TriangulatedSet.rank_eq_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S.rank = T.rank ↔ S.length = T.length ∧ ∀ (k : ℕ), S k ≈ T k

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

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

Equations

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

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

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

Equations

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

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

Equations

• TriangulatedSet.instDecidableLT = decidableLTOfDecidableLE

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

theorem TriangulatedSet.le_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ 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 TriangulatedSet.lt_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ R} : S < T ↔ S.rank < T.rank

theorem TriangulatedSet.lt_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangulatedSet σ 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 TriangulatedSet.lt_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : S ≠ ∅ → S < ∅

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

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

Equations

• x✝¹.instDecidableRelEquiv x✝ = instDecidableAnd

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

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

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

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

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

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

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

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

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

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

noncomputable def TriangulatedSet.single_of_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p ≠ 0) : TriangulatedSet σ R

Equations

• TriangulatedSet.single_of_ne_zero hp = { length' := 1, seq := fun (n : ℕ) => if n = 0 then p else 0, elements_ne_zero := ⋯, ascending_mainVariable := ⋯ }

theorem TriangulatedSet.single_of_ne_zero_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} {n : ℕ} (hp : p ≠ 0) : (single_of_ne_zero hp) n = if n = 0 then p else 0

theorem TriangulatedSet.length_single_of_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p ≠ 0) : (single_of_ne_zero hp).length = 1

Well-Foundedness

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

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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

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

noncomputable def TriangulatedSet.take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n : ℕ) : TriangulatedSet σ R

Equations

• S.take n = { length' := min n S.length, seq := fun (m : ℕ) => if m < n then S m else 0, elements_ne_zero := ⋯, ascending_mainVariable := ⋯ }

@[simp]

theorem TriangulatedSet.length_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n : ℕ) : (S.take n).length = min n S.length

theorem TriangulatedSet.take_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n m : ℕ) : (S.take n) m = if m < n then S m else 0

theorem TriangulatedSet.take_apply' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n m : ℕ} (h : m < min n S.length) : (S.take n) m = S m

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

@[simp]

theorem TriangulatedSet.take_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : S.take 0 = ∅

@[simp]

theorem TriangulatedSet.take_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : S.take S.length = S

theorem TriangulatedSet.take_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n : ℕ) : S.take n ⊆ S

theorem TriangulatedSet.toList_take_comm {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n : ℕ) : (S.take n).toList = List.take n S.toList

def TriangulatedSet.drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n : ℕ) : TriangulatedSet σ R

Equations

• S.drop n = { length' := S.length - n, seq := fun (m : ℕ) => S (m + n), elements_ne_zero := ⋯, ascending_mainVariable := ⋯ }

@[simp]

theorem TriangulatedSet.length_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n : ℕ) : (S.drop n).length = S.length - n

@[simp]

theorem TriangulatedSet.drop_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n m : ℕ) : (S.drop n) m = S (m + n)

@[simp]

theorem TriangulatedSet.drop_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : S.drop 0 = S

theorem TriangulatedSet.drop_eq_empty_of_ge_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {n : ℕ} : S.length ≤ n → S.drop n = ∅

@[simp]

theorem TriangulatedSet.drop_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) : S.drop S.length = ∅

theorem TriangulatedSet.toList_drop_comm {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (n : ℕ) : (S.drop n).toList = List.drop n S.toList

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

@[reducible, inline]

abbrev TriangulatedSet.canConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (p : MvPolynomial σ R) : Prop

The condition required to append p to S while maintaining the Triangulated Set property. p must be non-zero and its main variable must be strictly greater than the main variable of the last element of S.

Equations

• S.canConcat p = (p ≠ 0 ∧ (0 < S.length → (S (S.length - 1)).mainVariable < p.mainVariable))

theorem TriangulatedSet.canConcat_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} : S.canConcat p ↔ p ≠ 0 ∧ (0 < S.length → (S (S.length - 1)).mainVariable < p.mainVariable)

theorem TriangulatedSet.empty_canConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} : p ≠ 0 → ∅.canConcat p

theorem TriangulatedSet.not_canConcat_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} : ¬S.canConcat 0

noncomputable def TriangulatedSet.concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangulatedSet σ R) (p : MvPolynomial σ R) (h : S.canConcat p := by assumption) : TriangulatedSet σ R

Appends a polynomial p to the end of S. Requires S.canConcat p.

Equations

• S.concat p h = { length' := S.length + 1, seq := fun (n : ℕ) => if n < S.length then S n else if n = S.length then p else 0, elements_ne_zero := ⋯, ascending_mainVariable := ⋯ }

@[simp]

theorem TriangulatedSet.length_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) : (S.concat p h).length = S.length + 1

theorem TriangulatedSet.concat_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) (n : ℕ) : (S.concat p h) n = if n < S.length then S n else if n = S.length then p else 0

theorem TriangulatedSet.concat_apply_length {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) : (S.concat p h) S.length = p

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

theorem TriangulatedSet.mem_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) : p ∈ S.concat p h

theorem TriangulatedSet.subset_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) : S ⊆ S.concat p h

theorem TriangulatedSet.mem_concat_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p q : MvPolynomial σ R} (h : S.canConcat p) : q ∈ S.concat p h ↔ q = p ∨ q ∈ S

theorem TriangulatedSet.coe_concat_eq_insert {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) : ↑(S.concat p h) = Set.insert p ↑S

noncomputable def TriangulatedSet.list {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (h1 : ∀ p ∈ l, p ≠ 0 := by assumption) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l := by assumption) : TriangulatedSet σ R

Converts a list to a TriangulatedSet. Requires the list to be non-zero and pairwise strictly ascending in main variable.

Equations

• TriangulatedSet.list l h1 h2 = { length' := l.length, seq := fun (n : ℕ) => l.getD n 0, elements_ne_zero := ⋯, ascending_mainVariable := ⋯ }

theorem TriangulatedSet.length_list {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {l : List (MvPolynomial σ R)} (h1 : ∀ p ∈ l, p ≠ 0) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) : (list l h1 h2).length = l.length

theorem TriangulatedSet.list_nil_eq_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {l : List (MvPolynomial σ R)} (h1 : ∀ p ∈ l, p ≠ 0) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) (h3 : l = []) : list l h1 h2 = ∅

theorem TriangulatedSet.list_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {l : List (MvPolynomial σ R)} (h1 : ∀ p ∈ l, p ≠ 0) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) {n : ℕ} (hn : n < l.length) : (list l h1 h2) n = l[n]

theorem TriangulatedSet.toList_list_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {l : List (MvPolynomial σ R)} (h1 : ∀ p ∈ l, p ≠ 0) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) : (list l h1 h2).toList = l

theorem TriangulatedSet.list_eq_of_eq_toList {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangulatedSet σ R} {l : List (MvPolynomial σ R)} (h1 : ∀ p ∈ l, p ≠ 0) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) (heq : l = S.toList) : list l h1 h2 = S

theorem TriangulatedSet.mem_list_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {l : List (MvPolynomial σ R)} (h1 : ∀ p ∈ l, p ≠ 0) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) {p : MvPolynomial σ R} : p ∈ list l h1 h2 ↔ p ∈ l

noncomputable def TriangulatedSet.list! {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) : TriangulatedSet σ R

Unsafely construct a TriangulatedSet from a list. Panics if preconditions are not met. This should be used with caution, primarily for computation where inputs are guaranteed correct.

Equations

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

theorem TriangulatedSet.list!_eq_list {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (h1 : ∀ p ∈ l, p ≠ 0) (h2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) : list! l = list l h1 h2

noncomputable def TriangulatedSet.single {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (p : MvPolynomial σ R) : TriangulatedSet σ R

Equations

• TriangulatedSet.single p = if h : p = 0 then ∅ else TriangulatedSet.single_of_ne_zero h

@[simp]

theorem TriangulatedSet.single_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : single 0 = ∅

theorem TriangulatedSet.length_single {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} : p ≠ 0 → (single p).length = 1

theorem TriangulatedSet.single_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} : p = 0 ↔ single p = ∅

theorem TriangulatedSet.length_single_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} : p = 0 → (single p).length = 0

theorem TriangulatedSet.length_single_le_one {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} : (single p).length ≤ 1

theorem TriangulatedSet.single_apply_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (p : MvPolynomial σ R) : (single p) 0 = p

theorem TriangulatedSet.single_apply_nonzero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {n : ℕ} [DecidableEq R] (p : MvPolynomial σ R) : n ≠ 0 → (single p) n = 0

theorem TriangulatedSet.mem_single_of_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p : MvPolynomial σ R} : p ≠ 0 → p ∈ single p

theorem TriangulatedSet.notMem_single_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {p q : MvPolynomial σ R} : q ≠ p → q ∉ single p

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

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

theorem TriangulatedSet.single_of_length_le_one {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangulatedSet σ R} : S.length ≤ 1 → S = single (S 0)

theorem TriangulatedSet.single_of_last_mainVariable_eq_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangulatedSet σ R} : (S (S.length - 1)).mainVariable = ⊥ → S = single (S 0)

noncomputable def TriangulatedSet.takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangulatedSet σ R) (p : MvPolynomial σ R) : TriangulatedSet σ R

takeConcat S p tries to construct a new Triangulated Set by taking a prefix of S and appending p. This is a key operation in constructing the Characteristic Set. If p fits naturally at the end of S, it behaves like S.concat p. If p conflicts with some element in S (in terms of main variable order), takeConcat finds the first element in S that has a higher or equal main variable than p, truncates S before that element, and appends p.

Equations

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

theorem TriangulatedSet.takeConcat_eq_concat_of_canConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) : S.takeConcat p = S.concat p h

theorem TriangulatedSet.takeConcat_zero_eq_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangulatedSet σ R) : S.takeConcat 0 = ∅

theorem TriangulatedSet.mem_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangulatedSet σ R) {p : MvPolynomial σ R} (h : p ≠ 0) : p ∈ S.takeConcat p

theorem TriangulatedSet.takeConcat_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (q : MvPolynomial σ R) : q ∈ S.takeConcat p → q ≠ p → q ∈ S

theorem TriangulatedSet.reducedTo_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (q : MvPolynomial σ R) : q.reducedToSet ∅

theorem TriangulatedSet.reducedToSet_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangulatedSet σ R} {q : MvPolynomial σ R} : q.reducedToSet S ↔ ∀ i < S.length, q.reducedTo (S i)

noncomputable instance TriangulatedSet.instDecidableRelReducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : DecidableRel MvPolynomial.reducedToSet

Equations

• TriangulatedSet.instDecidableRelReducedToSet x✝ S = decidable_of_iff (∀ i < S.length, x✝.reducedTo (S i)) ⋯

theorem TriangulatedSet.reducedToSet_congr_right {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S T : TriangulatedSet σ R} {q : MvPolynomial σ R} : S ≈ T → (q.reducedToSet S ↔ q.reducedToSet T)

theorem TriangulatedSet.takeConcat_lt_of_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (p_ne_zero : p ≠ 0) (hp : p.reducedToSet S) : S.takeConcat p < S

Key Lemma for the Basic Set Algorithm: If p is non-zero and reduced with respect to S, then modifying S by appending p (using takeConcat) strictly decreases the rank of the triangulated set. This rank decrease is what guarantees the termination of the characteristic set computation.