Ascending sets and basic sets

This file defines the abstract theory of ascending sets and basic sets. An ascending set is a triangular set with additional reduction properties. A basic set is the "smallest" ascending set contained in a given set of polynomials.

Main declarations

• AscendingSetTheory: A typeclass abstracting the definition of an ascending set (e.g., strong vs. weak reduction).
• HasBasicSet: A typeclass abstracting the algorithm to compute a basic set from a list of polynomials.

class AscendingSetTheory (σ : Type u_1) (R : Type u_2) [CommSemiring R] [DecidableEq R] [LinearOrder σ] : Type (max u_1 u_2)

The abstract theory of Ascending Sets. This class allows us to define what it means for a TriangularSet to be an "Ascending Set". Different instances can implement Ritt's strong ascending sets or Wu's weak ascending sets.

• reducedTo' : MvPolynomial σ R → MvPolynomial σ R → Prop

  The reduction relation used to define the ascending property.

• decidableReducedTo : DecidableRel AscendingSetTheory.reducedTo'
• initial_reducedToSet_of_max_vars_ne_bot ⦃S : TriangularSet σ R⦄ ⦃i : ℕ⦄ : (∀ ⦃i j : ℕ⦄, i < j → j < S.length → AscendingSetTheory.reducedTo' (S j) (S i)) → (S i).vars.max ≠ ⊥ → (S i).initial.reducedToSet S

  A key property linking the ascending set structure to the initial. If S is an ascending set, the initial of any non-constant element in S must be reduced with respect to S.

def TriangularSet.IsAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] (S : TriangularSet σ R) : Prop

A Triangular Set is an Ascending Set if every element is reduced with respect to its predecessors.

Equations

• S.IsAscendingSet = ∀ ⦃i j : ℕ⦄, i < j → j < S.length → AscendingSetTheory.reducedTo' (S j) (S i)

theorem TriangularSet.isAscendingSet_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : TriangularSet σ R} : S.IsAscendingSet ↔ ∀ j < S.length, ∀ i < j, AscendingSetTheory.reducedTo' (S j) (S i)

@[implicit_reducible]

noncomputable instance TriangularSet.instDecidablePredIsAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] : DecidablePred IsAscendingSet

Equations

• x✝.instDecidablePredIsAscendingSet = decidable_of_iff (∀ j < x✝.length, ∀ i < j, AscendingSetTheory.reducedTo' (x✝ j) (x✝ i)) ⋯

theorem TriangularSet.isAscendingSet_single {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] (p : MvPolynomial σ R) : (single p).IsAscendingSet

theorem TriangularSet.isAscendingSet_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] : ∅.IsAscendingSet

theorem TriangularSet.isAscendingSet_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : TriangularSet σ R} (n : ℕ) : S.IsAscendingSet → (S.take n).IsAscendingSet

theorem TriangularSet.isAscendingSet_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : TriangularSet σ R} (n : ℕ) : S.IsAscendingSet → (S.drop n).IsAscendingSet

theorem TriangularSet.isAscendingSet_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) (hp : ∀ i < S.length, AscendingSetTheory.reducedTo' p (S i)) : S.IsAscendingSet → (S.concat p h).IsAscendingSet

theorem TriangularSet.isAscendingSet_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (hp : ∀ i < S.length, AscendingSetTheory.reducedTo' p (S i)) : S.IsAscendingSet → (S.takeConcat p).IsAscendingSet

def AscendingSet (σ : Type u_3) (R : Type u_4) [CommSemiring R] [LinearOrder σ] [DecidableEq R] [AscendingSetTheory σ R] : Type (max 0 u_3 u_4)

The type of Ascending Sets, which are Triangular Sets satisfying the ascending property.

Equations

• AscendingSet σ R = { TS : TriangularSet σ R // TS.IsAscendingSet }

class HasBasicSet (σ : Type u_3) (R : Type u_4) [CommSemiring R] [DecidableEq R] [LinearOrder σ] extends AscendingSetTheory σ R : Type (max u_3 u_4)

The interface for algorithms computing Basic Sets. Any instance of this class provides a basicSet function that computes a minimal ascending set contained in a given list of polynomials.

• reducedTo' : MvPolynomial σ R → MvPolynomial σ R → Prop
• decidableReducedTo : DecidableRel AscendingSetTheory.reducedTo'
• initial_reducedToSet_of_max_vars_ne_bot ⦃S : TriangularSet σ R⦄ ⦃i : ℕ⦄ : (∀ ⦃i j : ℕ⦄, i < j → j < S.length → AscendingSetTheory.reducedTo' (S j) (S i)) → (S i).vars.max ≠ ⊥ → (S i).initial.reducedToSet S
• basicSet : List (MvPolynomial σ R) → TriangularSet σ R

  Computes a Basic Set from a list of polynomials.

• basicSet_isAscendingSet (l : List (MvPolynomial σ R)) : (basicSet l).IsAscendingSet

  The output is always an Ascending Set.

• basicSet_subset (l : List (MvPolynomial σ R)) ⦃c : MvPolynomial σ R⦄ : c ∈ basicSet l → c ∈ l

  The output is a subset of the input.

• basicSet_minimal (l : List (MvPolynomial σ R)) ⦃S : TriangularSet σ R⦄ : S.IsAscendingSet → (∀ ⦃p : MvPolynomial σ R⦄, p ∈ S → p ∈ l) → basicSet l ≤ S

  Minimality condition: the output is ≤ any other ascending set contained in the input.

• basicSet_append_lt_of_exists_reducedToSet ⦃l1 l2 : List (MvPolynomial σ R)⦄ : (∃ p ∈ l2, p ≠ 0 ∧ p.reducedToSet (basicSet l1)) → basicSet (l2 ++ l1) < basicSet l1

  Order reduction property: appending a reduced element strictly decreases the basic set order. Crucial for proving termination of zero decomposition.

def StandardAscendingSet.IsAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (S : TriangularSet σ R) : Prop

Definition of Standard (Ritt) Ascending Set: strict degree reduction.

Equations

• StandardAscendingSet.IsAscendingSet S = ∀ ⦃i j : ℕ⦄, i < j → j < S.length → (S j).reducedTo (S i)

def WeakAscendingSet.IsAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (S : TriangularSet σ R) : Prop

Definition of Weak (Wu) Ascending Set: initial reduction.

Equations

• WeakAscendingSet.IsAscendingSet S = ∀ ⦃i j : ℕ⦄, i < j → j < S.length → (S j).initial.reducedTo (S i)

theorem WeakAscendingSet.isAscendingSet_of_isStandardAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} : StandardAscendingSet.IsAscendingSet S → IsAscendingSet S

theorem AscendingSet.initial_reducedToSet_of_max_vars_ne_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : TriangularSet σ R} {i : ℕ} : S.IsAscendingSet → (S i).vars.max ≠ ⊥ → (S i).initial.reducedToSet S

theorem AscendingSet.initial_reducedToSet_of_max_vars_ne_bot' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {p : MvPolynomial σ R} {S : TriangularSet σ R} (h : S.IsAscendingSet) : p ∈ S → p.vars.max ≠ ⊥ → p.initial.reducedToSet S

def AscendingSet.mk' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : TriangularSet σ R} (h : S.IsAscendingSet) : AscendingSet σ R

Construct an ascending set from a triangular set and a proof of the ascending property.

Equations

• AscendingSet.mk' h = ⟨S, h⟩

@[implicit_reducible]

instance AscendingSet.instCoeTriangularSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] : Coe (AscendingSet σ R) (TriangularSet σ R)

Equations

• AscendingSet.instCoeTriangularSet = { coe := Subtype.val }

@[simp]

theorem AscendingSet.coe_mk {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : AscendingSet σ R} (h : (↑S).IsAscendingSet) : ⟨↑S, h⟩ = S

theorem AscendingSet.coe_mk' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] (S : TriangularSet σ R) (h : S.IsAscendingSet) : ↑⟨S, h⟩ = S

theorem AscendingSet.eq_of_coe_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} (h : ↑S = ↑T) : S = T

theorem AscendingSet.ne_of_coe_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} (h : ↑S ≠ ↑T) : S ≠ T

theorem AscendingSet.coe_eq_coe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} : ↑S = ↑T ↔ S = T

theorem AscendingSet.coe_ne_coe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} : ↑S ≠ ↑T ↔ S ≠ T

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

The length of the ascending set.

Equations

• S.length = (↑S).length

theorem AscendingSet.length_coe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : AscendingSet σ R} : S.length = (↑S).length

@[implicit_reducible]

noncomputable instance AscendingSet.instFunLikeNatMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] : FunLike (AscendingSet σ R) ℕ (MvPolynomial σ R)

Equations

• AscendingSet.instFunLikeNatMvPolynomial = { coe := fun (S : AscendingSet σ R) => ⇑↑S, coe_injective' := ⋯ }

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

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

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

@[implicit_reducible]

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

Equations

• AscendingSet.instSetLike = { coe := fun (S : AscendingSet σ R) => ↑↑S, coe_injective' := ⋯ }

theorem AscendingSet.mem_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : AscendingSet σ R} {p : MvPolynomial σ R} : p ∈ S ↔ p ∈ ↑S

@[implicit_reducible]

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

Equations

• AscendingSet.instHasSubset = { Subset := InvImage (fun (x1 x2 : TriangularSet σ R) => x1 ⊆ x2) Subtype.val }

@[implicit_reducible]

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

Equations

• AscendingSet.instHasSSubset = { SSubset := InvImage (fun (x1 x2 : TriangularSet σ R) => x1 ⊂ x2) Subtype.val }

theorem AscendingSet.subset_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} : S ⊆ T ↔ ↑S ⊆ ↑T

theorem AscendingSet.ssubset_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} : S ⊂ T ↔ ↑S ⊂ ↑T

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

Converts a ascending set to a finite set.

Equations

• S.toFinset = (↑S).toFinset

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

Converts a ascending set to a list.

Equations

• S.toList = (↑S).toList

@[implicit_reducible]

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

Equations

• AscendingSet.instEmptyCollection = { emptyCollection := ⟨∅, ⋯⟩ }

@[implicit_reducible]

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

Equations

• AscendingSet.instInhabited = { default := ∅ }

theorem AscendingSet.empty_coe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] : ↑∅ = ∅

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

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

The order on the ascending set is exactly the order on the underlying triangular set.

Equations

• S.order = (↑S).order

theorem AscendingSet.order_coe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S : AscendingSet σ R} : S.order = (↑S).order

@[implicit_reducible]

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

Equations

• AscendingSet.instPreorder = Preorder.lift Subtype.val

theorem AscendingSet.lt_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} : S < T ↔ ↑S < ↑T

theorem AscendingSet.le_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} : S ≤ T ↔ ↑S ≤ ↑T

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• AscendingSet.instDecidableLT = decidableLTOfDecidableLE

@[implicit_reducible]

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

Equations

• AscendingSet.instSetoid = Setoid.comap Subtype.val inferInstance

@[implicit_reducible]

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

Equations

• x✝¹.instDecidableRelEquiv x✝ = instDecidableAnd

theorem AscendingSet.equiv_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] {S T : AscendingSet σ R} : S ≈ T ↔ ↑S ≈ ↑T

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

@[implicit_reducible]

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

Equations

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

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

theorem AscendingSet.Set.has_min' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] [Finite σ] (S' : Set (AscendingSet σ R)) (h : S'.Nonempty) : ∃ (S : AscendingSet σ R), Minimal (fun (x : AscendingSet σ R) => x ∈ S') S

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

The minimal element of a nonempty set of ascending sets.

Equations

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

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

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

@[implicit_reducible]

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

Equations

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

theorem MvPolynomial.Classical.hasBasicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] [Finite σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (a : α) : ∃ (S : AscendingSet σ R), Minimal (fun (a' : AscendingSet σ R) => ∀ ⦃p : MvPolynomial σ R⦄, p ∈ a' → p ∈ a) S

The main variableical existence of a Basic Set for any set of polynomials a. This is guaranteed by the well-foundedness of the order.

noncomputable def MvPolynomial.Classical.basicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] [Finite σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (a : α) : AscendingSet σ R

Non-computable choice of a Basic Set for a.

Equations

• MvPolynomial.Classical.basicSet a = ⋯.choose

theorem MvPolynomial.Classical.basicSet_minimal' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [AscendingSetTheory σ R] [Finite σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (a : α) : Minimal (fun (a' : AscendingSet σ R) => ∀ ⦃p : MvPolynomial σ R⦄, p ∈ a' → p ∈ a) (Classical.basicSet a)

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

The Basic Set of a list l, as computed by the HasBasicSet instance.

Equations

• MvPolynomial.List.basicSet l = ⟨HasBasicSet.basicSet l, ⋯⟩

theorem MvPolynomial.List.basicSet_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : ↑(basicSet l) ⊆ {p : MvPolynomial σ R | p ∈ l}

theorem MvPolynomial.List.basicSet_minimal {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) ⦃S : AscendingSet σ R⦄ : ↑S ⊆ {p : MvPolynomial σ R | p ∈ l} → basicSet l ≤ S

theorem MvPolynomial.List.basicSet_toList_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : basicSet (basicSet l).toList ≈ basicSet l

theorem MvPolynomial.List.basicSet_ge_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] {l1 l2 : List (MvPolynomial σ R)} : l1 ⊆ l2 → basicSet l2 ≤ basicSet l1

theorem MvPolynomial.List.basicSet_append_comm {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] {l1 l2 : List (MvPolynomial σ R)} : basicSet (l1 ++ l2) ≈ basicSet (l2 ++ l1)

theorem MvPolynomial.List.basicSet_append_lt_of_exists_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] {l1 l2 : List (MvPolynomial σ R)} (h : ∃ p ∈ l2, p ≠ 0 ∧ p.reducedToSet (basicSet l1)) : basicSet (l2 ++ l1) < basicSet l1

theorem TriangularSet.basicSet_toList_le_of_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] {S : TriangularSet σ R} (hS : S.IsAscendingSet) : ↑(MvPolynomial.List.basicSet S.toList) ≤ S