The Collins projection set

For a finite family F of univariate polynomials over a commutative ring R, the Collins projection F.collinsProjection is a finite subset of R. Write T for the set of all reducta of all members of F. The projection contains

• every coefficient r.coeff i, i ≤ r.natDegree, of every r ∈ T;
• every principal subresultant coefficient of r and r.derivative for r ∈ T;
• every principal subresultant coefficient of r and s for r, s ∈ T,

where the principal subresultant coefficients are taken at the actual degrees of the reducta, at every index from zero through the smaller of the two degrees. Zero and constant entries, and pairs coming from the same member of F, are retained: this gives a simple finite superset of Collins' projection which needs no preprocessing of the family.

The intended coefficient ring is R = MvPolynomial (Fin n) A, so that F is a family of polynomials in one distinguished variable over the base coordinates. Specializing the base coordinates is a ring homomorphism φ : R →+* S, and it can lower degrees. Truncation and principal coefficients are taken before specialization, and the reducta account for every possible drop in degree. The coefficients of p.map φ are the images of the coefficients of p, which lie in the projection. For commutative-ring targets, the specialization lemmas show that pairwise principal subresultant coefficients at the actual specialized degrees are also images under φ of elements of the projection; the derivative case requires an additively torsion-free target. Thus the signs of the projection at a base point determine the degrees of the specialized polynomials and, through the subresultant gcd criterion, the degrees of their pairwise gcds and of their gcds with their derivatives. This is how the projection enters Collins' delineability theorem.

The last section compares two specializations under which the same elements of the projection vanish, for instance evaluation at two points of a base set on which the projection is sign-invariant. Degrees and nullified members agree for arbitrary semiring targets. Pairwise principal subresultant coefficients have the same zero patterns for commutative-ring targets; the derivative case requires additively torsion-free targets. Pairwise gcd degrees agree for field targets, and gcd degrees with derivatives agree for additively torsion-free field targets. In characteristic-zero fields, a member that splits under both specializations has the same number of distinct roots; algebraically closed fields satisfy the splitting hypotheses.

Main definitions and results

• Finset.collinsProjection: the Collins projection set of a finite family.
• Finset.mem_collinsProjection: the explicit description of its elements.
• Finset.collinsProjection_mono: the projection is monotone in the family.
• Finset.collinsProjection_image_map: an injective coefficient map commutes with projection.
• Finset.collinsProjection_image_finSuccEquiv'_map, Finset.collinsProjection_image_finSuccEquiv_map: for a family of polynomials in n + 1 variables, singling out a variable and projecting commutes with an injective coefficient map. In particular the projection of a family with integer coefficients, viewed over ℝ, is the image of the projection computed entirely over ℤ.
• Finset.psc_map_mem_image_collinsProjection, Finset.psc_map_derivative_mem_image_collinsProjection: principal subresultant coefficients of specialized polynomials, at the specialized degrees, come from the projection. The derivative case requires an additively torsion-free target.
• Finset.natDegree_map_eq_of_collinsProjection, Finset.map_eq_zero_iff_of_collinsProjection: two specializations into arbitrary semirings under which the same elements of the projection vanish give every member of the family the same degree, and nullify the same members.
• Finset.natDegree_gcd_map_eq_of_collinsProjection, Finset.natDegree_gcd_map_derivative_eq_of_collinsProjection: under the same hypothesis, the specialized pairwise gcds have the same degrees over fields. The gcds with derivatives have the same degrees over additively torsion-free fields.
• Finset.card_roots_toFinset_map_eq_of_collinsProjection_of_splits: over characteristic-zero fields, a member that splits under both specializations has the same number of distinct roots.
• Finset.card_roots_toFinset_map_eq_of_collinsProjection: the algebraically closed case.

References

• G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Lecture Notes in Computer Science 33 (1975), 134–183.
• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 5 and 11.
• D. Jovanović, Solving Non-Linear Arithmetic, dissertation, New York University, 2012, Definition 2.5 and Theorem 2.6.

noncomputable def Finset.collinsProjection {R : Type u_1} [CommRing R] (F : Finset (Polynomial R)) : Finset R

The Collins projection of a finite family of polynomials. With T the set of all reducta of members of F, it consists of all coefficients of members of T, and the principal subresultant coefficients of (r, r.derivative) and of (r, s) for r, s ∈ T, at the actual degrees of these polynomials and at every index through the smaller degree.

theorem Finset.mem_collinsProjection {R : Type u_1} [CommRing R] {F : Finset (Polynomial R)} {a : R} : a ∈ F.collinsProjection ↔ (∃ p ∈ F, ∃ r ∈ p.reducta, ∃ i ≤ r.natDegree, r.coeff i = a) ∨ (∃ p ∈ F, ∃ r ∈ p.reducta, ∃ j ≤ min r.natDegree (Polynomial.derivative r).natDegree, r.psc (Polynomial.derivative r) r.natDegree (Polynomial.derivative r).natDegree j = a) ∨ ∃ p ∈ F, ∃ r ∈ p.reducta, ∃ q ∈ F, ∃ s ∈ q.reducta, ∃ j ≤ min r.natDegree s.natDegree, r.psc s r.natDegree s.natDegree j = a

The elements of the Collins projection: coefficients of reducta, principal subresultant coefficients of a reductum and its derivative, and principal subresultant coefficients of two reducta, all at actual degrees.

theorem Finset.coeff_mem_collinsProjection {R : Type u_1} [CommRing R] {F : Finset (Polynomial R)} {p r : Polynomial R} (hp : p ∈ F) (hr : r ∈ p.reducta) {i : ℕ} (hi : i ≤ r.natDegree) : r.coeff i ∈ F.collinsProjection

Every coefficient of a reductum of a member of the family, up to its degree, lies in the Collins projection.

theorem Finset.psc_derivative_mem_collinsProjection {R : Type u_1} [CommRing R] {F : Finset (Polynomial R)} {p r : Polynomial R} (hp : p ∈ F) (hr : r ∈ p.reducta) {j : ℕ} (hj : j ≤ min r.natDegree (Polynomial.derivative r).natDegree) : r.psc (Polynomial.derivative r) r.natDegree (Polynomial.derivative r).natDegree j ∈ F.collinsProjection

The principal subresultant coefficients of a reductum of a member of the family and its derivative, at their actual degrees, lie in the Collins projection.

theorem Finset.psc_mem_collinsProjection {R : Type u_1} [CommRing R] {F : Finset (Polynomial R)} {p q r s : Polynomial R} (hp : p ∈ F) (hr : r ∈ p.reducta) (hq : q ∈ F) (hs : s ∈ q.reducta) {j : ℕ} (hj : j ≤ min r.natDegree s.natDegree) : r.psc s r.natDegree s.natDegree j ∈ F.collinsProjection

The principal subresultant coefficients of two reducta of members of the family, at their actual degrees, lie in the Collins projection.

@[simp]

theorem Finset.collinsProjection_empty {R : Type u_1} [CommRing R] : ∅.collinsProjection = ∅

The Collins projection of the empty family is empty.

theorem Finset.collinsProjection_mono {R : Type u_1} [CommRing R] {F G : Finset (Polynomial R)} (h : F ⊆ G) : F.collinsProjection ⊆ G.collinsProjection

Enlarging the family enlarges its Collins projection.

theorem Finset.collinsProjection_image_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (F : Finset (Polynomial R)) : (image (Polynomial.map φ) F).collinsProjection = image (⇑φ) F.collinsProjection

An injective coefficient map commutes with the Collins projection. Injectivity preserves the degrees of all reducta and of their derivatives, so the principal subresultant coefficients are taken at the same formal bounds before and after the map. Without injectivity degrees can drop, and the two sides use different bounds.

theorem Finset.collinsProjection_image_finSuccEquiv'_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} [DecidableEq (MvPolynomial (Fin n) S)] [DecidableEq (Polynomial (MvPolynomial (Fin n) R))] [DecidableEq (Polynomial (MvPolynomial (Fin n) S))] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (P : Finset (MvPolynomial (Fin (n + 1)) R)) (i : Fin (n + 1)) : (image (fun (f : MvPolynomial (Fin (n + 1)) R) => (MvPolynomial.finSuccEquiv' S i) ((MvPolynomial.map φ) f)) P).collinsProjection = image (⇑(MvPolynomial.map φ)) (image (⇑(MvPolynomial.finSuccEquiv' R i)) P).collinsProjection

Projection of multivariate families along an injective coefficient map. Let P be a finite family of polynomials in the variables X 0, …, X n over R, viewed as polynomials in the distinguished variable X i over the polynomials in the other variables. Mapping the coefficients along an injective φ : R →+* S before singling out X i gives a family whose Collins projection is the image of the Collins projection computed over R.

theorem Finset.collinsProjection_image_finSuccEquiv_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} [DecidableEq (MvPolynomial (Fin n) S)] [DecidableEq (Polynomial (MvPolynomial (Fin n) R))] [DecidableEq (Polynomial (MvPolynomial (Fin n) S))] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (P : Finset (MvPolynomial (Fin (n + 1)) R)) : (image (fun (f : MvPolynomial (Fin (n + 1)) R) => (MvPolynomial.finSuccEquiv S n) ((MvPolynomial.map φ) f)) P).collinsProjection = image (⇑(MvPolynomial.map φ)) (image (⇑(MvPolynomial.finSuccEquiv R n)) P).collinsProjection

Projection of multivariate families along an injective coefficient map, for the distinguished variable X 0 singled out by MvPolynomial.finSuccEquiv. For φ = Int.castRingHom ℝ, this says that the Collins projection of a family of polynomials with integer coefficients, read over ℝ, is the image of the Collins projection computed entirely over ℤ.

theorem Finset.psc_map_mem_image_collinsProjection {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [DecidableEq S] (φ : R →+* S) {F : Finset (Polynomial R)} {p q : Polynomial R} (hp : p ∈ F) (hq : q ∈ F) {j : ℕ} (hj : j ≤ min (Polynomial.map φ p).natDegree (Polynomial.map φ q).natDegree) : (Polynomial.map φ p).psc (Polynomial.map φ q) (Polynomial.map φ p).natDegree (Polynomial.map φ q).natDegree j ∈ image (⇑φ) F.collinsProjection

Specialization of principal subresultant coefficients. For members p, q of the family and any coefficient map φ, the principal subresultant coefficients of p.map φ and q.map φ at their actual degrees are images of elements of the Collins projection. The witnesses are the corresponding coefficients of the reducta cut off just above the specialized degrees.

theorem Finset.psc_map_derivative_mem_image_collinsProjection {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [HasUniqueDiv S] [DecidableEq S] (φ : R →+* S) {F : Finset (Polynomial R)} {p : Polynomial R} (hp : p ∈ F) {j : ℕ} (hj : j ≤ min (Polynomial.map φ p).natDegree (Polynomial.derivative (Polynomial.map φ p)).natDegree) : (Polynomial.map φ p).psc (Polynomial.derivative (Polynomial.map φ p)) (Polynomial.map φ p).natDegree (Polynomial.derivative (Polynomial.map φ p)).natDegree j ∈ image (⇑φ) F.collinsProjection

Specialization of derivative principal subresultant coefficients. For a member p of the family and a coefficient map φ into an additively torsion-free ring, the principal subresultant coefficients of p.map φ and its derivative at their actual degrees are images of elements of the Collins projection. Torsion-freeness ensures that the specialized derivative has the expected degree; in positive characteristic the derivative of a reductum can drop further in degree under specialization.

Invariance of the specialized family

Throughout, φ and ψ are two specializations under which the same elements of the Collins projection vanish. Nullification and degree invariance allow arbitrary semiring targets. The zero patterns of pairwise principal subresultant coefficients agree for commutative-ring targets, with additively torsion-free targets required for the derivative case. Pairwise gcd degrees agree for field targets, and gcd degrees with derivatives agree for additively torsion-free field targets. Root-count invariance requires characteristic-zero fields and splitting of the member under both specializations; the algebraically closed case follows.

theorem Finset.map_eq_zero_iff_of_collinsProjection {R : Type u_1} [CommRing R] {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] {φ : R →+* A} {ψ : R →+* B} {F : Finset (Polynomial R)} {p : Polynomial R} (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) : Polynomial.map φ p = 0 ↔ Polynomial.map ψ p = 0

If the same elements of the Collins projection vanish under φ and ψ, then a member of the family is nullified by φ exactly when it is nullified by ψ.

theorem Finset.natDegree_map_eq_of_collinsProjection {R : Type u_1} [CommRing R] {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] {φ : R →+* A} {ψ : R →+* B} {F : Finset (Polynomial R)} {p : Polynomial R} (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) : (Polynomial.map φ p).natDegree = (Polynomial.map ψ p).natDegree

If the same elements of the Collins projection vanish under φ and ψ, then every member of the family has the same degree after either specialization.

theorem Finset.psc_map_eq_zero_iff_of_collinsProjection {R : Type u_1} [CommRing R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] {φ : R →+* A} {ψ : R →+* B} {F : Finset (Polynomial R)} {p q : Polynomial R} (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) (hq : q ∈ F) {j : ℕ} (hj : j ≤ min (Polynomial.map φ p).natDegree (Polynomial.map φ q).natDegree) : (Polynomial.map φ p).psc (Polynomial.map φ q) (Polynomial.map φ p).natDegree (Polynomial.map φ q).natDegree j = 0 ↔ (Polynomial.map ψ p).psc (Polynomial.map ψ q) (Polynomial.map ψ p).natDegree (Polynomial.map ψ q).natDegree j = 0

If the same elements of the Collins projection vanish under φ and ψ, then for two members of the family the principal subresultant coefficients of their specializations, at the specialized degrees, vanish at the same indices.

theorem Finset.psc_map_derivative_eq_zero_iff_of_collinsProjection {R : Type u_1} [CommRing R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] {φ : R →+* A} {ψ : R →+* B} {F : Finset (Polynomial R)} {p : Polynomial R} [HasUniqueDiv A] [HasUniqueDiv B] (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) {j : ℕ} (hj : j ≤ min (Polynomial.map φ p).natDegree (Polynomial.derivative (Polynomial.map φ p)).natDegree) : (Polynomial.map φ p).psc (Polynomial.derivative (Polynomial.map φ p)) (Polynomial.map φ p).natDegree (Polynomial.derivative (Polynomial.map φ p)).natDegree j = 0 ↔ (Polynomial.map ψ p).psc (Polynomial.derivative (Polynomial.map ψ p)) (Polynomial.map ψ p).natDegree (Polynomial.derivative (Polynomial.map ψ p)).natDegree j = 0

If the same elements of the Collins projection vanish under φ and ψ, then for a member of the family the principal subresultant coefficients of its specialization and their derivative, at the specialized degrees, vanish at the same indices. The targets are additively torsion-free, so that the derivative of a specialization has the expected degree.

theorem Finset.natDegree_gcd_map_eq_of_collinsProjection {R : Type u_1} [CommRing R] {K : Type u_3} {L : Type u_4} [Field K] [Field L] [DecidableEq K] [DecidableEq L] {φ : R →+* K} {ψ : R →+* L} {F : Finset (Polynomial R)} {p q : Polynomial R} (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) (hq : q ∈ F) : (EuclideanDomain.gcd (Polynomial.map φ p) (Polynomial.map φ q)).natDegree = (EuclideanDomain.gcd (Polynomial.map ψ p) (Polynomial.map ψ q)).natDegree

If the same elements of the Collins projection vanish under φ and ψ, then for any two members of the family the gcds of their specializations have the same degree.

theorem Finset.natDegree_gcd_map_derivative_eq_of_collinsProjection {R : Type u_1} [CommRing R] {K : Type u_3} {L : Type u_4} [Field K] [Field L] [DecidableEq K] [DecidableEq L] {φ : R →+* K} {ψ : R →+* L} {F : Finset (Polynomial R)} {p : Polynomial R} [HasUniqueDiv K] [HasUniqueDiv L] (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) : (EuclideanDomain.gcd (Polynomial.map φ p) (Polynomial.derivative (Polynomial.map φ p))).natDegree = (EuclideanDomain.gcd (Polynomial.map ψ p) (Polynomial.derivative (Polynomial.map ψ p))).natDegree

If the same elements of the Collins projection vanish under φ and ψ, then for every member of the family the gcd of its specialization with its derivative has the same degree under both specializations. The targets are additively torsion-free.

theorem Finset.card_roots_toFinset_map_eq_of_collinsProjection_of_splits {R : Type u_1} [CommRing R] {K : Type u_3} {L : Type u_4} [Field K] [Field L] [DecidableEq K] [DecidableEq L] {φ : R →+* K} {ψ : R →+* L} {F : Finset (Polynomial R)} {p : Polynomial R} [CharZero K] [CharZero L] (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) (hφ : (Polynomial.map φ p).Splits) (hψ : (Polynomial.map ψ p).Splits) : (Polynomial.map φ p).roots.toFinset.card = (Polynomial.map ψ p).roots.toFinset.card

If two specializations into characteristic-zero fields nullify the same elements of the Collins projection and a member splits under both specializations, then it has the same number of distinct roots after either specialization. The zero polynomial has an empty root multiset by convention.

theorem Finset.card_roots_toFinset_map_eq_of_collinsProjection {R : Type u_1} [CommRing R] {K : Type u_3} {L : Type u_4} [Field K] [Field L] [DecidableEq K] [DecidableEq L] {φ : R →+* K} {ψ : R →+* L} {F : Finset (Polynomial R)} {p : Polynomial R} [CharZero K] [CharZero L] [IsAlgClosed K] [IsAlgClosed L] (h : ∀ a ∈ F.collinsProjection, φ a = 0 ↔ ψ a = 0) (hp : p ∈ F) : (Polynomial.map φ p).roots.toFinset.card = (Polynomial.map ψ p).roots.toFinset.card

If the same elements of the Collins projection vanish under specializations φ and ψ into algebraically closed fields of characteristic zero, then every member of the family has the same number of distinct roots after either specialization. A member nullified by one is nullified by both, and Polynomial.roots of the zero polynomial is empty by convention, so both counts are then zero.