Bézout identities for subresultant polynomials

At every index, the fixed-bound subresultant polynomial is a combination A * q + B * p, where A and B have degrees below m - j and n - j, respectively. Outside the strict range j < min m n, the subresultant is zero and both coefficients can be chosen zero. The identity holds over any commutative ring, including rings with zero divisors, and allows the actual degrees of the inputs to be smaller than their formal bounds. Consequently every common divisor of the inputs divides the subresultant polynomial.

These identities place subresultants in the ideal generated by the inputs and allow common factors to be tracked through the subresultant family. No invertibility or nonvanishing of a principal subresultant coefficient is required.

Main results

• TauCeti.exists_mul_add_mul_eq_subresultant: the Bézout identity with strict degree bounds.
• TauCeti.dvd_subresultant: every common divisor divides the fixed-bound subresultant.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4: the determinant construction of subresultant Bézout identities.

theorem TauCeti.exists_mul_add_mul_eq_subresultant {R : Type u_1} [CommRing R] {p q : Polynomial R} {m n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) : ∃ (A : Polynomial R) (B : Polynomial R), A.degree < ↑(m - j) ∧ B.degree < ↑(n - j) ∧ A * q + B * p = p.subresultant q m n j

At every index, a subresultant polynomial is a Bézout combination of its inputs. The coefficients of q and p have degrees strictly below m - j and n - j, respectively. The formal bounds may exceed the actual degrees, and neither input nor the subresultant is required to be nonzero. Outside the strict range, both Bézout coefficients can be zero.

theorem TauCeti.dvd_subresultant {R : Type u_1} [CommRing R] {p q d : Polynomial R} {m n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hp : d ∣ p) (hq : d ∣ q) : d ∣ p.subresultant q m n j

Every common divisor of the inputs divides their fixed-bound subresultant polynomial. This also covers indices outside the strict range, where the subresultant polynomial is zero.