Pseudo-Division

This file defines pseudo-division of multivariate polynomials, a fundamental operation in the Characteristic Set Method.

Main Definitions

• MvPolynomial.pseudoOf: Pseudo-division of g by f with respect to a variable i (over commutative rings).
• MvPolynomial.pseudo: General pseudo-division that handles constants and zero (over fields).
• MvPolynomial.setPseudo: Successive pseudo-division by all polynomials in a triangular set.
• MvPolynomial.setPseudoRem: Computes only the remainder (more efficient when quotients are not needed).
• MvPolynomial.isRemainder: A predicate stating that r is a valid remainder of g by f, meaning r is reduced w.r.t. f and init(f)^s * g = q * f + r for some s, q.
• MvPolynomial.isSetRemainder: A predicate stating that r is a valid remainder of g by a triangular set S, meaning r is reduced w.r.t. S and satisfies the extended division equation.

Main Theorems

• pseudoOf_equation: init(f) ^ s * g = q * f + r where deg(r) < deg(f)
• pseudoOf_remainder_reducedTo: The remainder is reduced w.r.t. the divisor
• pseudo_remainder_isRemainder: The remainder satisfies the isRemainder predicate
• setPseudo_remainder_isSetRemainder: The remainder satisfies the isSetRemainder predicate
• setPseudo_remainder_eq_zero_of_mem: Elements of S have zero remainder when divided by S

structure MvPolynomial.PseudoResult (α : Type u_1) : Type u_1

The result of a pseudo-division of g by f. exponent is the power s such that init(f) ^ s * g = quotient * f + remainder.

• exponent : ℕ
• quotient : α
• remainder : α

structure MvPolynomial.SetPseudoResult (α : Type u_1) : Type u_1

The result of pseudo-dividing g by a sequence of polynomials (a triangulated set). exponents and quotients correspond to each step of the division.

• exponents : List ℕ
• quotients : List α
• remainder : α

noncomputable def MvPolynomial.pseudoOf {R : Type u_1} {σ : Type u_2} [CommRing R] (i : σ) (g f : MvPolynomial σ R) : PseudoResult (MvPolynomial σ R)

Pseudo-division of g by f regarding the variable i. This algorithm computes q and r such that initᵢ(f) ^ s * g = q * f + r, where degᵢ(r) < degᵢ(f). It uses a fuel parameter to guarantee termination.

Equations

• MvPolynomial.pseudoOf i g f = MvPolynomial.pseudoOf.go i f (MvPolynomial.initialOf i f) (MvPolynomial.degreeOf i f) (MvPolynomial.degreeOf i g + 1 - MvPolynomial.degreeOf i f) 0 0 g

@[irreducible]

noncomputable def MvPolynomial.pseudoOf.go {R : Type u_1} {σ : Type u_2} [CommRing R] (i : σ) (f I : MvPolynomial σ R) (n fuel s : ℕ) (q r : MvPolynomial σ R) : PseudoResult (MvPolynomial σ R)

Equations

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

@[simp]

theorem MvPolynomial.zero_pseudoOf {R : Type u_1} {σ : Type u_2} [CommRing R] (i : σ) (f : MvPolynomial σ R) : pseudoOf i 0 f = { exponent := 1 - degreeOf i f, quotient := 0, remainder := 0 }

@[simp]

theorem MvPolynomial.pseudoOf_self {R : Type u_1} {σ : Type u_2} [CommRing R] (i : σ) (f : MvPolynomial σ R) : pseudoOf i f f = { exponent := 1, quotient := initialOf i f, remainder := 0 }

theorem MvPolynomial.pseudoOfGo_next {R : Type u_1} {σ : Type u_2} [CommRing R] {i : σ} (f I : MvPolynomial σ R) {n : ℕ} (fuel s : ℕ) (q : MvPolynomial σ R) {r : MvPolynomial σ R} (hn : n ≤ degreeOf i r) : have term := initialOf i r * X i ^ (degreeOf i r - n); pseudoOf.go i f I n (fuel + 1) s q r = pseudoOf.go i f I n fuel (s + 1) (I * q + term) (I * r - term * f)

theorem MvPolynomial.pseudoOfGo_equation {R : Type u_1} {σ : Type u_2} [CommRing R] (i : σ) (g f I : MvPolynomial σ R) (n fuel s : ℕ) (q r : MvPolynomial σ R) : I ^ s * g = q * f + r → I ^ (pseudoOf.go i f I n fuel s q r).exponent * g = (pseudoOf.go i f I n fuel s q r).quotient * f + (pseudoOf.go i f I n fuel s q r).remainder

theorem MvPolynomial.pseudoOf_equation {R : Type u_1} {σ : Type u_2} [CommRing R] (i : σ) (g f : MvPolynomial σ R) : initialOf i f ^ (pseudoOf i g f).exponent * g = (pseudoOf i g f).quotient * f + (pseudoOf i g f).remainder

The fundamental equation of pseudo-division: initᵢ(f) ^ s * g = q * f + r

theorem MvPolynomial.degreeOf_pseudoOfGo_remainder_le_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] {i j : σ} {f I : MvPolynomial σ R} (n : ℕ) (hi : i ≠ j) (hj : degreeOf j f = 0) (hI : I = initialOf i f) (fuel s : ℕ) (q r : MvPolynomial σ R) : degreeOf j (pseudoOf.go i f I n fuel s q r).remainder ≤ degreeOf j r

theorem MvPolynomial.degreeOf_pseudoOf_remainder_le_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] {i j : σ} (g : MvPolynomial σ R) {f : MvPolynomial σ R} (hi : i ≠ j) (hj : degreeOf j f = 0) : degreeOf j (pseudoOf i g f).remainder ≤ degreeOf j g

theorem MvPolynomial.dvd_pseudoOf_remainder_of_dvd {R : Type u_1} {σ : Type u_2} [CommRing R] (i : σ) {g f : MvPolynomial σ R} (h : f ∣ g) : f ∣ (pseudoOf i g f).remainder

theorem MvPolynomial.pseudoOf_remainder_eq_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] {i : σ} {g f : MvPolynomial σ R} (h1 : degreeOf i g = 0) (h2 : degreeOf i f ≠ 0) : (pseudoOf i g f).remainder = g

theorem MvPolynomial.degreeOf_pseudoOfGo_remainder_lt_of_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i : σ} {f I : MvPolynomial σ R} {n : ℕ} (hI : I = initialOf i f) (hn : n ≠ 0) (hnd : n = degreeOf i f) (fuel s : ℕ) (q r : MvPolynomial σ R) : fuel ≥ degreeOf i r + 1 - n → degreeOf i (pseudoOf.go i f I n fuel s q r).remainder < degreeOf i f

theorem MvPolynomial.degreeOf_pseudoOf_remainder_lt_of_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i : σ} (g : MvPolynomial σ R) {f : MvPolynomial σ R} (hi : degreeOf i f ≠ 0) : degreeOf i (pseudoOf i g f).remainder < degreeOf i f

theorem MvPolynomial.pseudoOf_remainder_eq_zero_of_dvd {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i : σ} {g f : MvPolynomial σ R} (h1 : f ∣ g) (h2 : degreeOf i f ≠ 0) : (pseudoOf i g f).remainder = 0

theorem MvPolynomial.pseudoOf_remainder_reducedTo {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] [DecidableEq R] [LinearOrder σ] {c : σ} (g : MvPolynomial σ R) {f : MvPolynomial σ R} (hc : f.mainVariable = ↑c) : (pseudoOf c g f).remainder.reducedTo f

def MvPolynomial.isRemainder {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g f : MvPolynomial σ R) : Prop

A remainder r of g by f is a polynomial which is reduced with respect to f and suffices f.initial ^ s * g = q * f + r for some s : ℕ and q : R[σ].

Equations

• r.isRemainder g f = (r.reducedTo f ∧ ∃ (s : ℕ) (q : MvPolynomial σ R), f.initial ^ s * g = q * f + r)

theorem MvPolynomial.isRemainder_def {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g f : MvPolynomial σ R) : r.isRemainder g f ↔ r.reducedTo f ∧ ∃ (s : ℕ) (q : MvPolynomial σ R), f.initial ^ s * g = q * f + r

def MvPolynomial.isSetRemainder {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g : MvPolynomial σ R) (S : TriangulatedSet σ R) : Prop

A remainder r of g by S is a polynomial which is reduced with respect to S and suffices (∏ i, (S i).initial ^ es[i]) * g = (∑ i, qs[i] * S i) + r for some es : List ℕ and qs : List R[σ].

Equations

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

theorem MvPolynomial.isSetRemainder_def {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g : MvPolynomial σ R) (S : TriangulatedSet σ R) : r.isSetRemainder g S ↔ r.reducedToSet S ∧ ∃ (es : List ℕ) (qs : List (MvPolynomial σ R)), (es.length = S.length ∧ qs.length = S.length) ∧ (∏ i : Fin es.length, (S ↑i).initial ^ es[i]) * g = ∑ i : Fin qs.length, qs[i] * S ↑i + r

noncomputable def MvPolynomial.pseudo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) : PseudoResult (MvPolynomial σ R)

General pseudo-division of g by f. If f is constant, it performs standard division. If f is non-constant, it performs pseudo-division with respect to mainVariable(f).

Equations

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

@[simp]

theorem MvPolynomial.pseudo_zero {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g : MvPolynomial σ R} : g.pseudo 0 = { exponent := 0, quotient := 0, remainder := g }

@[simp]

theorem MvPolynomial.pseudo_C {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g : MvPolynomial σ R} {r : R} (hr : r ≠ 0) : g.pseudo (C r) = { exponent := 0, quotient := r⁻¹ • g, remainder := 0 }

@[simp]

theorem MvPolynomial.zero_pseudo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : MvPolynomial σ R) : pseudo 0 f = { exponent := 0, quotient := 0, remainder := 0 }

@[simp]

theorem MvPolynomial.pseudo_remainder_self {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : MvPolynomial σ R) : (f.pseudo f).remainder = 0

theorem MvPolynomial.pseudo_of_mainVariable_isSome {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) {c : σ} {f : MvPolynomial σ R} : f.mainVariable = ↑c → g.pseudo f = pseudoOf c g f

theorem MvPolynomial.pseudo_equation {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) : f.initial ^ (g.pseudo f).exponent * g = (g.pseudo f).quotient * f + (g.pseudo f).remainder

theorem MvPolynomial.degreeOf_pseudo_remainder_le_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {i : σ} (g : MvPolynomial σ R) {f : MvPolynomial σ R} (h : degreeOf i f = 0) : degreeOf i (g.pseudo f).remainder ≤ degreeOf i g

theorem MvPolynomial.pseudo_remainder_reducedTo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) (h : f ≠ 0) : (g.pseudo f).remainder.reducedTo f

theorem MvPolynomial.pseudo_remainder_isRemainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) (h : f ≠ 0) : (g.pseudo f).remainder.isRemainder g f

theorem MvPolynomial.isRemainder_of_eq_pseudo_remainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {r g f : MvPolynomial σ R} (h : f ≠ 0) : (g.pseudo f).remainder = r → r.isRemainder g f

theorem MvPolynomial.pseudo_remainder_eq_zero_of_dvd {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g f : MvPolynomial σ R} (h : f ∣ g) : (g.pseudo f).remainder = 0

theorem MvPolynomial.pseudo_remainder_eq_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g f : MvPolynomial σ R} {c : σ} (h1 : f.mainVariable = some c) (h2 : degreeOf c g = 0) : (g.pseudo f).remainder = g

noncomputable def MvPolynomial.setPseudo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : SetPseudoResult (MvPolynomial σ R)

Pseudo-divides g successively by elements of S. Typically, this involves dividing by Sₗ₋₁, then Sₗ₋₂, ..., down to S₀.

Equations

• g.setPseudo S = MvPolynomial.setPseudo.go (⇑S) S.length [] [] g

@[irreducible]

noncomputable def MvPolynomial.setPseudo.go {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : ℕ → MvPolynomial σ R) (fuel : ℕ) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : SetPseudoResult (MvPolynomial σ R)

Equations

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

theorem MvPolynomial.length_setPseudoGo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : ℕ → MvPolynomial σ R) (fuel : ℕ) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : (setPseudo.go f fuel es qs r).exponents.length = es.length + fuel ∧ (setPseudo.go f fuel es qs r).quotients.length = qs.length + fuel

theorem MvPolynomial.length_setPseudo_exponents {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : (g.setPseudo S).exponents.length = S.length

theorem MvPolynomial.length_setPseudo_quotients {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : (g.setPseudo S).quotients.length = S.length

theorem MvPolynomial.setPseudoGo_equation {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (f : ℕ → MvPolynomial σ R) (fuel : ℕ) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : List.foldrIdx (fun (i e : ℕ) (I : MvPolynomial σ R) => (f i).initial ^ e * I) 1 es fuel * g = List.foldrIdx (fun (i : ℕ) (q Q : MvPolynomial σ R) => q * f i + Q) 0 qs fuel + r → List.foldrIdx (fun (i e : ℕ) (I : MvPolynomial σ R) => (f i).initial ^ e * I) 1 (setPseudo.go f fuel es qs r).exponents * g = List.foldrIdx (fun (i : ℕ) (q Q : MvPolynomial σ R) => q * f i + Q) 0 (setPseudo.go f fuel es qs r).quotients + (setPseudo.go f fuel es qs r).remainder

theorem MvPolynomial.setPseudo_equation' {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : List.foldrIdx (fun (i e : ℕ) (I : MvPolynomial σ R) => (S i).initial ^ e * I) 1 (g.setPseudo S).exponents * g = List.foldrIdx (fun (i : ℕ) (q Q : MvPolynomial σ R) => q * S i + Q) 0 (g.setPseudo S).quotients + (g.setPseudo S).remainder

theorem MvPolynomial.setPseudo_equation {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : (∏ i : Fin (g.setPseudo S).exponents.length, (S ↑i).initial ^ (g.setPseudo S).exponents[i]) * g = ∑ i : Fin (g.setPseudo S).quotients.length, (g.setPseudo S).quotients[i] * S ↑i + (g.setPseudo S).remainder

noncomputable def MvPolynomial.setPseudoRem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : MvPolynomial σ R

The remainder of pseudo-dividing g by the set S. This is computationally simpler than setPseudo if only the remainder is needed.

Equations

• g.setPseudoRem S = List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) g S.toList

theorem MvPolynomial.zero_setPseudoRem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) : List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) 0 l = 0

theorem MvPolynomial.setPseudoGo_drop_succ_remainder_eq {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (S : TriangulatedSet σ R) {k n : ℕ} (hn : n < k) (hk : k ≤ S.length) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : (setPseudo.go (⇑(S.drop (k - (n + 1)))) (n + 1) es qs r).remainder = ((setPseudo.go (⇑(S.drop (k - n))) n es qs r).remainder.pseudo (S (k - (n + 1)))).remainder

theorem MvPolynomial.setPseudo_remainder_eq_setPseudoRem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : (g.setPseudo S).remainder = g.setPseudoRem S

theorem MvPolynomial.setPseudoRem_reducedTo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (hl1 : ∀ ⦃p : MvPolynomial σ R⦄, p ∈ l → p ≠ 0) (hl2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) (g p : MvPolynomial σ R) : p ∈ l → (List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) g l).reducedTo p

theorem MvPolynomial.setPseudo_remainder_reducedToSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : (g.setPseudo S).remainder.reducedToSet S

theorem MvPolynomial.setPseudo_remainder_isSetRemainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangulatedSet σ R) : (g.setPseudo S).remainder.isSetRemainder g S

theorem MvPolynomial.isSetRemainder_of_eq_setPseudo_remainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {r g : MvPolynomial σ R} {S : TriangulatedSet σ R} : (g.setPseudo S).remainder = r → r.isSetRemainder g S

theorem MvPolynomial.setPseudoRem_eq_self_of_mainVariable_lt {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (hl1 : ∀ ⦃p : MvPolynomial σ R⦄, p ∈ l → p ≠ 0) (hl2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.mainVariable < q.mainVariable) l) ⦃g : MvPolynomial σ R⦄ : (∀ p ∈ l, g.mainVariable < p.mainVariable) → List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) g l = g

theorem MvPolynomial.setPseudo_remainder_eq_zero_of_mem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (S : TriangulatedSet σ R) {p : MvPolynomial σ R} (hp : p ∈ S) : (p.setPseudo S).remainder = 0