Standard Ascending Set (Ritt's Definition)

This file implements the theory and algorithm for Standard Ascending Set. In this context, a "Standard Ascending Set" requires that every element is reduced with respect to preceding elements.

Main Instances

• AscendingSetTheory: Implements the theory using reducedTo (strong reduction).
• HasBasicSet: Provides the basicSet algorithm that computes a minimal standard ascending set from a list of polynomials.

theorem StandardAscendingSet.isAscendingSet_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangulatedSet σ R} : isAscendingSet S ↔ ∀ ⦃i j : ℕ⦄, i < j → j < S.length → (S j).reducedTo (S i)

theorem StandardAscendingSet.isAscendingSet_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangulatedSet σ R} : isAscendingSet S ↔ ∀ ⦃i j : ℕ⦄, i < j → i < S.length → (S j).reducedTo (S i)

theorem StandardAscendingSet.reducedTo_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangulatedSet σ R} {i j : ℕ} (h : isAscendingSet S) : i ≠ j → j < S.length → (S i).reducedTo (S j)

noncomputable def StandardAscendingSet.instAscendingSetTheory {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : AscendingSetTheory σ R

The standard ascending set theory uses strong reduction reducedTo.

Equations

• StandardAscendingSet.instAscendingSetTheory = { reducedTo' := MvPolynomial.reducedTo, decidableReducedTo := inferInstance, initial_reducedToSet_of_mainVariable_ne_bot := ⋯ }

theorem StandardAscendingSet.isAscendingSet_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (h : S.canConcat p) (hp : p.reducedToSet S) : S.isAscendingSet → (S.concat p h).isAscendingSet

theorem StandardAscendingSet.isAscendingSet_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangulatedSet σ R} {p : MvPolynomial σ R} (hp : p.reducedToSet S) : S.isAscendingSet → (S.takeConcat p).isAscendingSet

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

Computes the Standard Basic Set of a list of polynomials. The algorithm works by:

1. Sort the list and let BS = ∅.
2. Pick the first (minimal) element B in the list.
3. Update the current basic set BS with B using takeConcat (which handles replacements).
4. Filter the remaining list to keep only elements reduced w.r.t. the new BS and go to step 2.

Equations

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

@[irreducible]

noncomputable def StandardAscendingSet.basicSet.go {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangulatedSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : TriangulatedSet σ R

Equations

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

theorem StandardAscendingSet.basicSetGo_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangulatedSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (h : l ≠ []) : (l.head h).reducedToSet BS → basicSet.go l BS hl1 < BS

theorem StandardAscendingSet.basicSetGo_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangulatedSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : Option.all (fun (p : MvPolynomial σ R) => decide (p.reducedToSet BS)) l.head? = true → basicSet.go l BS hl1 ≤ BS

theorem StandardAscendingSet.mem_of_mem_basicSetGo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangulatedSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (p : MvPolynomial σ R) : p ∉ BS → p ∈ basicSet.go l BS hl1 → p ∈ l

theorem StandardAscendingSet.basicSetGo_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangulatedSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : Option.all (fun (p : MvPolynomial σ R) => decide (p.reducedToSet BS)) l.head? = true → BS.isAscendingSet → (basicSet.go l BS hl1).isAscendingSet

theorem StandardAscendingSet.basicSetGo_le_ascendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangulatedSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : List.Pairwise (fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2) l → (∀ p ∈ l, BS.canConcat p) → Option.all (fun (x : MvPolynomial σ R) => decide (x.reducedToSet BS)) l.head? = true → ∀ (T : TriangulatedSet σ R), T.isAscendingSet → (BS.length ≤ T.length ∧ ∀ i < BS.length, BS i ≈ T i) → (∀ p ∈ T, (∀ i < BS.length, ¬BS i ≈ p) → p ∈ l) → basicSet.go l BS hl1 ≤ T

The core lemma proving that the computed Basic Set is indeed minimal among all ascending sets contained in l.

noncomputable def StandardAscendingSet.instHasBasicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : HasBasicSet σ R

The Standard Basic Set algorithm satisfies the abstract HasBasicSet interface.

Equations

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