The McCallum projection set

Let F be a finite family of polynomials in one distinguished variable over a commutative ring R with a normalized gcd, and let B be a basis of F: in McCallum's setting, a finite set of primitive, squarefree, pairwise coprime polynomials of positive degree whose products of powers recover the members of F up to their contents. The McCallum projection F.mcCallumProjection B is the finite subset of R consisting of

• the content f.content of every member f ∈ F;
• every coefficient b.coeff i, i ≤ b.natDegree, of every member b ∈ B;
• the discriminant b.discr of every member b ∈ B;
• the resultant resultant b b' of every pair of distinct members b, b' ∈ B, in both orders (which differ only by a sign).

The intended coefficient ring is R = MvPolynomial (Fin n) ℝ with B an irreducible basis of F (Finset.IsIrreducibleBasis), or more generally a squarefree basis (Finset.IsSquarefreeBasis). Mathlib fixes no normalization on MvPolynomial; any NormalizedGCDMonoid structure may be chosen, and changing it changes each content only by a unit factor.

Unlike the Collins projection Finset.collinsProjection, no reducta and no subresultant coefficients beyond resultants and discriminants are taken. McCallum proves that this smaller set suffices for lifting over a base cell on which every element of the projection is order-invariant (rather than merely sign-invariant) and no member of the basis is nullified. The contents are always included, so that information about the members of F is not lost when passing to the basis.

The projection depends on the choice of basis only up to associates: two irreducible bases of the same family give projections whose elements are associated to one another (Finset.IsIrreducibleBasis.exists_associated_mem_mcCallumProjection). Since associated multivariate polynomials over a field differ by a nonzero constant factor, whether every element of the projection is sign-invariant, or order-invariant, on a set does not depend on the basis.

Specializing the base coordinates is a ring homomorphism φ : R →+* A. The last section shows that the zero pattern of the projection under a specialization fixes the degrees and the nullified members of both the basis and the family: if the same elements of the projection vanish under φ and ψ, then every member of the basis, and every member of the family, has the same degree after either specialization, and is nullified by φ exactly when it is nullified by ψ.

The discriminant of the product of any subfamily of a squarefree basis has constant ambient order wherever the projection does (Finset.IsSquarefreeBasis.orderAt_discr_prod_eq_of_mcCallumProjection). Together with Finset.IsSquarefreeBasis.discr_prod_ne_zero, this supplies the discriminant hypotheses for applying a single-polynomial delineability theorem to the active basis product.

Main definitions and results

• Finset.mcCallumProjection: the McCallum projection of a family with respect to a basis.
• Finset.mem_mcCallumProjection: the explicit description of its elements.
• Finset.mcCallumProjection_mono: the projection is monotone in the family and the basis.
• Finset.IsIrreducibleBasis.exists_associated_mem_mcCallumProjection: independence of the basis up to associates.
• Finset.natDegree_map_eq_of_mcCallumProjection, Finset.map_eq_zero_iff_of_mcCallumProjection: two specializations under which the same elements of the projection vanish give every member of the basis the same degree, and nullify the same members of the basis.
• Finset.IsSquarefreeBasis.natDegree_map_eq_of_mcCallumProjection, Finset.IsSquarefreeBasis.map_eq_zero_iff_of_mcCallumProjection: the same for the members of the family, when the basis is a squarefree basis.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), 242–268.

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

The McCallum projection of the family F with respect to the basis B: the contents of the members of F, together with the coefficients and discriminants of the members of B and the resultants of pairs of distinct members of B. Resultants and discriminants are taken at the actual degrees.

theorem Finset.mem_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {a : R} : a ∈ F.mcCallumProjection B ↔ (∃ f ∈ F, f.content = a) ∨ (∃ b ∈ B, ∃ i ≤ b.natDegree, b.coeff i = a) ∨ (∃ b ∈ B, b.discr = a) ∨ ∃ b ∈ B, ∃ b' ∈ B, b ≠ b' ∧ b.resultant b' = a

The elements of the McCallum projection: contents of members of the family, and coefficients, discriminants and pairwise resultants of members of the basis.

theorem Finset.content_mem_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {f : Polynomial R} (hf : f ∈ F) : f.content ∈ F.mcCallumProjection B

The content of every member of the family lies in the McCallum projection.

theorem Finset.coeff_mem_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b : Polynomial R} (hb : b ∈ B) {i : ℕ} (hi : i ≤ b.natDegree) : b.coeff i ∈ F.mcCallumProjection B

Every coefficient of a member of the basis, up to its degree, lies in the McCallum projection.

theorem Finset.discr_mem_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b : Polynomial R} (hb : b ∈ B) : b.discr ∈ F.mcCallumProjection B

The discriminant of every member of the basis lies in the McCallum projection.

theorem Finset.resultant_mem_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b b' : Polynomial R} (hb : b ∈ B) (hb' : b' ∈ B) (hne : b ≠ b') : b.resultant b' ∈ F.mcCallumProjection B

The resultant of two distinct members of the basis lies in the McCallum projection.

@[simp]

theorem Finset.mcCallumProjection_empty_right {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F : Finset (Polynomial R)} [DecidableEq R] : F.mcCallumProjection ∅ = image Polynomial.content F

With the empty basis, the McCallum projection consists of the contents of the family.

theorem Finset.mcCallumProjection_mono {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F F' B B' : Finset (Polynomial R)} (hF : F ⊆ F') (hB : B ⊆ B') : F.mcCallumProjection B ⊆ F'.mcCallumProjection B'

Enlarging the family or the basis enlarges the McCallum projection.

Independence of the basis

theorem Finset.IsIrreducibleBasis.exists_associated_mem_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B B' : Finset (Polynomial R)} [IsDomain R] (hB : F.IsIrreducibleBasis B) (hB' : F.IsIrreducibleBasis B') {a : R} (ha : a ∈ F.mcCallumProjection B') : ∃ a' ∈ F.mcCallumProjection B, Associated a a'

Independence of the basis. For two irreducible bases B and B' of the same family, every element of the McCallum projection with respect to B' is associated to an element of the McCallum projection with respect to B.

Specialization

Throughout, φ and ψ are two specializations under which the same elements of the McCallum projection vanish. The statements about the basis hold for specializations into arbitrary commutative rings; the statements about the family are over domains.

theorem Finset.map_eq_zero_iff_of_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b : Polynomial R} {A : Type u_2} {A' : Type u_3} [CommRing A] [CommRing A'] {φ : R →+* A} {ψ : R →+* A'} (h : ∀ a ∈ F.mcCallumProjection B, φ a = 0 ↔ ψ a = 0) (hb : b ∈ B) : Polynomial.map φ b = 0 ↔ Polynomial.map ψ b = 0

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

theorem Finset.natDegree_map_eq_of_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b : Polynomial R} {A : Type u_2} {A' : Type u_3} [CommRing A] [CommRing A'] {φ : R →+* A} {ψ : R →+* A'} (h : ∀ a ∈ F.mcCallumProjection B, φ a = 0 ↔ ψ a = 0) (hb : b ∈ B) : (Polynomial.map φ b).natDegree = (Polynomial.map ψ b).natDegree

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

theorem Finset.IsSquarefreeBasis.map_eq_zero_iff_of_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {f : Polynomial R} {A : Type u_2} {A' : Type u_3} [CommRing A] [CommRing A'] {φ : R →+* A} {ψ : R →+* A'} [IsDomain A] [IsDomain A'] (hB : F.IsSquarefreeBasis B) (h : ∀ a ∈ F.mcCallumProjection B, φ a = 0 ↔ ψ a = 0) (hf : f ∈ F) : Polynomial.map φ f = 0 ↔ Polynomial.map ψ f = 0

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

theorem Finset.IsSquarefreeBasis.natDegree_map_eq_of_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {f : Polynomial R} {A : Type u_2} {A' : Type u_3} [CommRing A] [CommRing A'] {φ : R →+* A} {ψ : R →+* A'} [IsDomain A] [IsDomain A'] (hB : F.IsSquarefreeBasis B) (h : ∀ a ∈ F.mcCallumProjection B, φ a = 0 ↔ ψ a = 0) (hf : f ∈ F) : (Polynomial.map φ f).natDegree = (Polynomial.map ψ f).natDegree

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

theorem Finset.IsSquarefreeBasis.orderAt_discr_prod_eq_of_mcCallumProjection {σ : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [NormalizedGCDMonoid (MvPolynomial σ R)] {F B A : Finset (Polynomial (MvPolynomial σ R))} (hB : F.IsSquarefreeBasis B) (hA : A ⊆ B) (a b : σ → R) (h : ∀ p ∈ F.mcCallumProjection B, p.orderAt a = p.orderAt b) : (∏ p ∈ A, p).discr.orderAt a = (∏ p ∈ A, p).discr.orderAt b

The McCallum projection determines the ambient order of the discriminant of the product of any subfamily of the basis. In particular, order-invariance of the projection supplies the constant-order hypothesis of the discriminant theorem for this product. The formal discriminant may vanish at both base points; no nonvanishing of its values or of specialized leading coefficients is assumed.