Characteristic Set Method (Wu's Method)

This file implements the core algorithms of Wu's Method for solving systems of algebraic equations.

Main Concepts

1. Characteristic Set (CS): A special triangular set contained in a polynomial set PS that generates the same ideal up to saturation by initials.
2. Zero Decomposition: The process of decomposing the zero set of PS into the union of zero sets of triangular sets. Zero(PS) = ⋃ Zero(CSᵢ/IPᵢ) where CSᵢ are triangular sets and IPᵢ are products of initials.

Main Algorithms

• MvPolynomial.List.characteristicSet: Computes a characteristic set of a list of polynomials.
• MvPolynomial.List.zeroDecomposition: Decomposes the zero set of a polynomial system into a finite set of triangular systems.

Main Theorems

• Well-Ordering Principles:
  • vanishingSet_diff_initialProd_subset: Zero(CS/IP) ⊆ Zero(PS)
  • vanishingSet_diff_initialProd_eq: Zero(CS/IP) = Zero(PS/IP)
  • vanishingSet_decomposition: Zero(PS) = Zero(CS/IP) ∪ ⋃_{CS} Zero(PS ∪ {init(p)})
• characteristicSet_isCharacteristicSet: The algorithm computes a valid characteristic set
• vanishingSet_eq_zeroDecomposition_union: Zero Decomposition Theorem. The variety of the input system is exactly the union of the "quasi-varieties" defined by the computed triangular sets.

Vanishing Sets

def MvPolynomial.vanishingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] {α : Type u_3} [Membership (MvPolynomial σ R) α] (K : Type u_4) [CommSemiring K] [Algebra R K] (a : α) : Set (σ → K)

The set of points in K ^ σ where all polynomials in a vanish. It is the same as zeroLocus K (Ideal.span a) for a : Set R[σ]

Equations

• MvPolynomial.vanishingSet K a = {x : σ → K | ∀ p ∈ a, (MvPolynomial.aeval x) p = 0}

theorem MvPolynomial.vanishingSet_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] {α : Type u_3} [Membership (MvPolynomial σ R) α] (K : Type u_4) [CommSemiring K] [Algebra R K] (a : α) : vanishingSet K a = {x : σ → K | ∀ p ∈ a, (aeval x) p = 0}

def MvPolynomial.singleVanishingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] (K : Type u_4) [CommSemiring K] [Algebra R K] (p : MvPolynomial σ R) : Set (σ → K)

The set of points where a single polynomial p vanishes.

Equations

• MvPolynomial.singleVanishingSet K p = {x : σ → K | (MvPolynomial.aeval x) p = 0}

theorem MvPolynomial.singleVanishingSet_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] (K : Type u_4) [CommSemiring K] [Algebra R K] (p : MvPolynomial σ R) : singleVanishingSet K p = {x : σ → K | (aeval x) p = 0}

theorem MvPolynomial.vanishingSet_singleton_eq_singleVanishingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] (K : Type u_4) [CommSemiring K] [Algebra R K] (p : MvPolynomial σ R) : vanishingSet K {p} = singleVanishingSet K p

theorem MvPolynomial.vanishingSet_eq_zeroLocus_span {R : Type u_1} {σ : Type u_2} [Field R] (K : Type u_3) [Field K] [Algebra R K] (PS : Set (MvPolynomial σ R)) : vanishingSet K PS = zeroLocus K (Ideal.span PS)

theorem MvPolynomial.vanishingSet_eq_zeroLocus_span' {R : Type u_1} {σ : Type u_2} [Field R] (K : Type u_3) [Field K] [Algebra R K] {α : Type u_4} [Membership (MvPolynomial σ R) α] (a : α) : vanishingSet K a = zeroLocus K (Ideal.span {p : MvPolynomial σ R | p ∈ a})

Characteristic Set Properties

def TriangulatedSet.isCharacteristicSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (K : Type u_4) [CommSemiring K] [Algebra R K] (CS : TriangulatedSet σ R) (a : α) : Prop

A Triangulated Set CS is a Characteristic Set for a if:

1. Every element in a reduce to 0 modulo CS.
2. Zero(a) ⊆ Zero(CS) (geometric containment).

Equations

• TriangulatedSet.isCharacteristicSet K CS a = ((∀ g ∈ a, MvPolynomial.isSetRemainder 0 g CS) ∧ MvPolynomial.vanishingSet K a ⊆ MvPolynomial.vanishingSet K CS)

theorem CharacteristicSet.vanishingSet_diff_initialProd_subset {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (K : Type u_4) [Field K] [Algebra R K] {PS : α} {CS : TriangulatedSet σ R} (h : ∀ g ∈ PS, MvPolynomial.isSetRemainder 0 g CS) : MvPolynomial.vanishingSet K CS \ MvPolynomial.singleVanishingSet K (MvPolynomial.initialProd CS.toFinset) ⊆ MvPolynomial.vanishingSet K PS

Well-Ordering Principle (1): Zero(CS/IP) ⊆ Zero(PS). If all polynomials in PS reduce to 0 modulo CS, then any zero of CS that isn't a zero of IP must be a zero of PS.

theorem CharacteristicSet.vanishingSet_diff_initialProd_eq {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (K : Type u_4) [Field K] [Algebra R K] {PS : α} {CS : TriangulatedSet σ R} (h : TriangulatedSet.isCharacteristicSet K CS PS) : MvPolynomial.vanishingSet K CS \ MvPolynomial.singleVanishingSet K (MvPolynomial.initialProd CS.toFinset) = MvPolynomial.vanishingSet K PS \ MvPolynomial.singleVanishingSet K (MvPolynomial.initialProd CS.toFinset)

Well-Ordering Principle (2): Zero(CS/IP) = Zero(PS/IP).

theorem CharacteristicSet.vanishingSet_decomposition {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (K : Type u_4) [Field K] [Algebra R K] {PS : α} {CS : TriangulatedSet σ R} (h : TriangulatedSet.isCharacteristicSet K CS PS) : MvPolynomial.vanishingSet K PS = MvPolynomial.vanishingSet K CS \ MvPolynomial.singleVanishingSet K (MvPolynomial.initialProd CS.toFinset) ∪ ⋃ p ∈ CS, MvPolynomial.vanishingSet K PS ∩ MvPolynomial.singleVanishingSet K p.initial

Well-Ordering Principle (3): Zero(PS) = Zero(CS/IP) ∪ ⋃_{CS} Zero(PS ∪ {init(p)})

Characteristic Set Algorithm

theorem MvPolynomial.List.characteristicSetGo_decreasing {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] (l₀ l : List (MvPolynomial σ R)) (BS : TriangulatedSet σ R) (lBS RS : List (MvPolynomial σ R)) (hRS : RS ≠ []) (hBS : BS = ↑(basicSet l)) (hlBS : lBS = BS.toList) (hRS1 : RS = List.filter (fun (x : MvPolynomial σ R) => decide (x ≠ 0)) (List.map (fun (p : MvPolynomial σ R) => (p.setPseudo BS).remainder) (l \ lBS))) : basicSet (l₀ ++ RS ++ lBS) < basicSet l

noncomputable def MvPolynomial.List.characteristicSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : TriangulatedSet σ R

Computes the Characteristic Set of a polynomial list l. Algorithm:

1. Let l₀ = l.
2. Compute BS = BasicSet(l).
3. Compute remainders RS of l \ BS with respect to BS.
4. If RS is empty, BS is the characteristic set.
5. If not, set l = l₀ ++ RS ++ BS and go to step 2. Termination is guaranteed by the well-ordering of ranks.

Equations

• MvPolynomial.List.characteristicSet l = MvPolynomial.List.characteristicSet.go l l

@[irreducible]

noncomputable def MvPolynomial.List.characteristicSet.go {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [HasBasicSet σ R] (l₀ : List (MvPolynomial σ R)) [Finite σ] (l : List (MvPolynomial σ R)) : TriangulatedSet σ R

Equations

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

theorem MvPolynomial.List.zero_isSetRemainder_characteristicSetGo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l₀ l : List (MvPolynomial σ R)) : l₀ ⊆ l → ∀ p ∈ l₀, isSetRemainder 0 p (characteristicSet.go l₀ l)

theorem MvPolynomial.List.characteristicSetGo_vanishingSet_subset {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (K : Type u_5) [CommSemiring K] [Algebra R K] (l₀ l : List (MvPolynomial σ R)) : vanishingSet K l₀ = vanishingSet K l → vanishingSet K l₀ ⊆ vanishingSet K (characteristicSet.go l₀ l)

theorem MvPolynomial.List.characteristicSet_isCharacteristicSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (K : Type u_5) [CommSemiring K] [Algebra R K] (l : List (MvPolynomial σ R)) : TriangulatedSet.isCharacteristicSet K (characteristicSet l) l

The computed characteristicSet satisfies the required properties.

theorem MvPolynomial.List.characteristicSetGo_le_basicSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l₀ l : List (MvPolynomial σ R)) : characteristicSet.go l₀ l ≤ ↑(basicSet l)

theorem MvPolynomial.List.characteristicSet_le_basicSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : characteristicSet l ≤ ↑(basicSet l)

theorem MvPolynomial.List.characteristicSetGo_isAscendingSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l₀ l : List (MvPolynomial σ R)) : (characteristicSet.go l₀ l).isAscendingSet

theorem MvPolynomial.List.characteristicSet_isAscendingSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : (characteristicSet l).isAscendingSet

def MvPolynomial.List.cs {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : TriangulatedSet σ R

Alias of MvPolynomial.List.characteristicSet.

---

Computes the Characteristic Set of a polynomial list l. Algorithm:

1. Let l₀ = l.
2. Compute BS = BasicSet(l).
3. Compute remainders RS of l \ BS with respect to BS.
4. If RS is empty, BS is the characteristic set.
5. If not, set l = l₀ ++ RS ++ BS and go to step 2. Termination is guaranteed by the well-ordering of ranks.

Equations

• @MvPolynomial.List.cs = @MvPolynomial.List.characteristicSet

theorem MvPolynomial.List.cs_isCharacteristicSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (K : Type u_5) [CommSemiring K] [Algebra R K] (l : List (MvPolynomial σ R)) : TriangulatedSet.isCharacteristicSet K (characteristicSet l) l

Alias of MvPolynomial.List.characteristicSet_isCharacteristicSet.

---

The computed characteristicSet satisfies the required properties.

theorem MvPolynomial.List.cs_le_basicSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : characteristicSet l ≤ ↑(basicSet l)

Alias of MvPolynomial.List.characteristicSet_le_basicSet.

theorem MvPolynomial.List.cs_isAscendingSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : (characteristicSet l).isAscendingSet

Alias of MvPolynomial.List.characteristicSet_isAscendingSet.

Zero Decomposition

@[irreducible]

noncomputable def MvPolynomial.List.zeroDecomposition {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) : List (TriangulatedSet σ R)

Decomposes the zero set of l into a union of zero sets of triangular sets. The algorithm recursively computes the characteristic set CS and adds branches for the initials of CS.

Equations

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

theorem MvPolynomial.List.isAscendingSet_of_mem_zeroDecomposition {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) (CS : TriangulatedSet σ R) : CS ∈ zeroDecomposition l → CS.isAscendingSet

theorem MvPolynomial.List.zero_isSetRemainder_of_mem_zeroDecomposition {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (l : List (MvPolynomial σ R)) (CS : TriangulatedSet σ R) : CS ∈ zeroDecomposition l → ∀ g ∈ l, isSetRemainder 0 g CS

theorem MvPolynomial.List.vanishingSet_eq_zeroDecomposition_union {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] [Finite σ] [HasBasicSet σ R] (K : Type u_6) [Field K] [Algebra R K] (l : List (MvPolynomial σ R)) : vanishingSet K l = ⋃ CS ∈ zeroDecomposition l, vanishingSet K CS \ singleVanishingSet K (initialProd CS.toFinset)

Zero Decomposition Theorem: The vanishing set of l is the union of the vanishing sets of the triangular sets in zeroDecomposition, excluding the zeros of their initials. Zero(l) = ⋃_{CS ∈ ZD(l)} Zero(CS/IP(CS)).