Squarefree bases of finite families of polynomials

Let D be a GCD domain and F a finite family of polynomials in one distinguished variable over D. A squarefree basis of F, in McCallum's sense, is a finite set B of primitive, squarefree polynomials of positive degree which are pairwise relatively prime, such that every member of F is a constant times a product of powers of members of B. The constant is the content of the member up to a unit, since products of primitive polynomials are primitive.

Every irreducible basis (Finset.IsIrreducibleBasis) is a squarefree basis, but the members of a squarefree basis need not be irreducible: over ℤ, {X ^ 2 - 1} is a squarefree basis of itself, and the nonconstant factors sᵢ of a factorization f = c * ∏ i, sᵢ ^ i of a single polynomial f into primitive, squarefree, pairwise relatively prime sᵢ form a squarefree basis of {f}. McCallum's family lifting theorem only uses the properties recorded here.

Over the fraction field the product of a squarefree basis stays squarefree and its members stay pairwise coprime, by Gauss's lemma. Hence the resultants of distinct members are nonzero, and in characteristic zero the discriminant of the product of any subfamily is nonzero.

The factorization of each member also reconstructs its roots and their multiplicities after any specialization into a domain that does not nullify the member: the multiplicity of a root is a weighted sum of its multiplicities in the specialized basis members, with exponents independent of the specialization and of the root. Specialized basis members may acquire common or multiple roots, and their contributions then add. This transfers invariant multiplicities on common root sections from the basis to the original family. Nullified members have multiplicity zero, following the convention of Polynomial.rootMultiplicity.

Main definitions and results

• Finset.IsSquarefreeBasis F B: B is a squarefree basis of the finite family F.
• Finset.IsSquarefreeBasis.exists_eq_C_content_mul_unit_mul_prod: every member of the family is its content times a unit times a product of powers of the basis.
• Finset.IsSquarefreeBasis.squarefree_prod, Finset.IsSquarefreeBasis.squarefree_prod_map: the product of the basis is squarefree, also over the fraction field.
• Finset.IsSquarefreeBasis.isCoprime_map, Finset.IsSquarefreeBasis.resultant_ne_zero: distinct members of the basis are coprime over the fraction field, so their resultant is nonzero.
• Finset.IsSquarefreeBasis.discr_prod_ne_zero, Finset.IsSquarefreeBasis.discr_ne_zero: in characteristic zero, the product of any subfamily of the basis, in particular each member, has nonzero discriminant.
• Finset.IsSquarefreeBasis.isRoot_map_iff: after a specialization φ : D →+* A into a domain under which a member f of the family does not vanish, the roots of the specialized f are exactly the roots of the specialized basis members dividing f.
• Finset.IsSquarefreeBasis.exists_rootMultiplicity_eq_sum, Finset.IsSquarefreeBasis.exists_rootMultiplicity_map_eq_sum: after any such specialization, the root multiplicities of the specialized f are a weighted sum of those of the specialized basis members, with weights independent of the specialization and of the root.
• Finset.IsSquarefreeBasis.rootMultiplicity_map_eq: equal basis multiplicities at two specialized points give equal multiplicities for every member of the family that is nullified by both specializations or by neither.

References

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

structure Finset.IsSquarefreeBasis {D : Type u_1} [CommRing D] (F B : Finset (Polynomial D)) : Prop

B is a squarefree basis of the finite family F of polynomials over D: its members are primitive, squarefree, of positive degree and pairwise relatively prime, and every member of F is a constant times a product of powers of members of B.

• isPrimitive (b : Polynomial D) : b ∈ B → b.IsPrimitive

  Every member of the basis is primitive.

• natDegree_pos (b : Polynomial D) : b ∈ B → 0 < b.natDegree

  Every member of the basis has positive degree.

• squarefree (b : Polynomial D) : b ∈ B → Squarefree b

  Every member of the basis is squarefree.

• isRelPrime (b : Polynomial D) : b ∈ B → ∀ b' ∈ B, b ≠ b' → IsRelPrime b b'

  Distinct members of the basis are relatively prime.

• exists_eq_C_mul_prod (f : Polynomial D) : f ∈ F → ∃ (c : D) (e : Polynomial D → ℕ), f = Polynomial.C c * ∏ b ∈ B, b ^ e b

  Every member of the family is a constant times a product of powers of the basis.

theorem Finset.IsSquarefreeBasis.isRoot_map_iff {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} (hB : F.IsSquarefreeBasis B) {f : Polynomial D} (hf : f ∈ F) {A : Type u_2} [CommRing A] [IsDomain A] (φ : D →+* A) (hφ : Polynomial.map φ f ≠ 0) (t : A) : (Polynomial.map φ f).IsRoot t ↔ ∃ b ∈ B, b ∣ f ∧ (Polynomial.map φ b).IsRoot t

Roots of a specialized member of the family are the roots of the specialized members of the basis dividing it, provided the specialization of the member does not vanish.

theorem Finset.IsSquarefreeBasis.isPrimitive_prod {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} [IsGCDMonoid D] (hB : F.IsSquarefreeBasis B) (e : Polynomial D → ℕ) : (∏ b ∈ B, b ^ e b).IsPrimitive

Every product of powers of the members of a squarefree basis is primitive, so the constant in exists_eq_C_mul_prod is the content of the member up to a unit.

theorem Finset.IsSquarefreeBasis.exists_eq_C_content_mul_unit_mul_prod {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} [NormalizedGCDMonoid D] (hB : F.IsSquarefreeBasis B) {f : Polynomial D} (hf : f ∈ F) : ∃ (u : Dˣ) (e : Polynomial D → ℕ), f = Polynomial.C (f.content * ↑u) * ∏ b ∈ B, b ^ e b

Every member of the family is its content, times a unit, times a product of powers of the members of a squarefree basis.

theorem Finset.IsSquarefreeBasis.exists_rootMultiplicity_eq_sum {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {A : Type u_2} [CommRing A] [IsDomain A] {f : Polynomial D} (hB : F.IsSquarefreeBasis B) (hf : f ∈ F) : ∃ (e : Polynomial D → ℕ), ∀ (φ : Polynomial D →*₀ Polynomial A), (∀ (c : D), ∃ (a : A), φ (Polynomial.C c) = Polynomial.C a) → φ f ≠ 0 → ∀ (t : A), Polynomial.rootMultiplicity t (φ f) = ∑ b ∈ B, e b * Polynomial.rootMultiplicity t (φ b)

One fixed exponent vector reconstructs root multiplicities under every zero-preserving multiplicative map that sends constants to constants and does not nullify the input. Additivity and preservation of degrees are not required.

theorem Finset.IsSquarefreeBasis.exists_rootMultiplicity_map_eq_sum {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {A : Type u_2} [CommRing A] [IsDomain A] {f : Polynomial D} (hB : F.IsSquarefreeBasis B) (hf : f ∈ F) : ∃ (e : Polynomial D → ℕ), ∀ (φ : D →+* A), Polynomial.map φ f ≠ 0 → ∀ (t : A), Polynomial.rootMultiplicity t (Polynomial.map φ f) = ∑ b ∈ B, e b * Polynomial.rootMultiplicity t (Polynomial.map φ b)

One fixed exponent vector reconstructs root multiplicities after every specialization that does not nullify the input. Neither injectivity of the coefficient map nor preservation of degrees or coprimality is required.

theorem Finset.IsSquarefreeBasis.rootMultiplicity_map_eq {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {A : Type u_2} [CommRing A] [IsDomain A] {f : Polynomial D} (hB : F.IsSquarefreeBasis B) (hf : f ∈ F) (φ ψ : D →+* A) (s t : A) (hzero : Polynomial.map φ f = 0 ↔ Polynomial.map ψ f = 0) (hm : ∀ b ∈ B, Polynomial.rootMultiplicity s (Polynomial.map φ b) = Polynomial.rootMultiplicity t (Polynomial.map ψ b)) : Polynomial.rootMultiplicity s (Polynomial.map φ f) = Polynomial.rootMultiplicity t (Polynomial.map ψ f)

Equal basis multiplicities at two specialized points give equal input multiplicities, provided the input is nullified by both maps or by neither. The two root values need not be equal, so this applies along moving sections.

theorem Finset.IsSquarefreeBasis.squarefree_prod {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} [IsDomain D] [IsGCDMonoid D] (hB : F.IsSquarefreeBasis B) : Squarefree (∏ b ∈ B, b)

The product of the members of a squarefree basis is squarefree.

theorem Finset.IsSquarefreeBasis.squarefree_prod_map {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} [IsDomain D] [IsGCDMonoid D] (K : Type u_2) [Field K] [Algebra D K] [IsFractionRing D K] (hB : F.IsSquarefreeBasis B) : Squarefree (∏ b ∈ B, Polynomial.map (algebraMap D K) b)

The product of the members of a squarefree basis is squarefree over the fraction field.

theorem Finset.IsSquarefreeBasis.discr_prod_ne_zero {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} [IsDomain D] [IsGCDMonoid D] [CharZero D] (hB : F.IsSquarefreeBasis B) {A : Finset (Polynomial D)} (hA : A ⊆ B) : (∏ b ∈ A, b).discr ≠ 0

In characteristic zero, the product of any subfamily of a squarefree basis has nonzero discriminant. This includes the empty subfamily, whose product is 1.

theorem Finset.IsSquarefreeBasis.discr_ne_zero {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {b : Polynomial D} [IsDomain D] [IsGCDMonoid D] [CharZero D] (hB : F.IsSquarefreeBasis B) (hb : b ∈ B) : b.discr ≠ 0

In characteristic zero, the discriminant of a member of a squarefree basis is nonzero.

theorem Finset.IsSquarefreeBasis.isCoprime_map {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {b b' : Polynomial D} [IsDomain D] [IsGCDMonoid D] (K : Type u_2) [Field K] [Algebra D K] [IsFractionRing D K] (hB : F.IsSquarefreeBasis B) (hb : b ∈ B) (hb' : b' ∈ B) (hne : b ≠ b') : IsCoprime (Polynomial.map (algebraMap D K) b) (Polynomial.map (algebraMap D K) b')

Distinct members of a squarefree basis are coprime over the fraction field.

theorem Finset.IsSquarefreeBasis.resultant_ne_zero {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {b b' : Polynomial D} [IsDomain D] [IsGCDMonoid D] (hB : F.IsSquarefreeBasis B) (hb : b ∈ B) (hb' : b' ∈ B) (hne : b ≠ b') : b.resultant b' ≠ 0

The resultant of two distinct members of a squarefree basis is nonzero.