Recovering a family delineation from its product

A delineation of the product of a finite family of nowhere-zero real polynomial fibers induces a delineation of the family, with exactly the same ordered root functions. The factors must have continuous coefficients and constant degrees, and the base must be nonempty and preconnected. Factors may share roots and have repeated roots.

The key point is that every factor multiplicity is locally bounded above, while their sum, the product multiplicity, is constant. Thus every factor multiplicity is locally constant, and preconnectedness makes it constant on the whole base. Sign-invariance then follows from the root coverage and connectedness of sections and sectors.

This allows a discriminant theorem applied to a single basis product to supply the common stack of its factors, without requiring pairwise coprimality of the fibers or nonvanishing specialized discriminants. The empty factor family is included: its product is one and the stack has no sections.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3 (delineability of a polynomial basis).

theorem TauCeti.Delineation.rootMultiplicity_eq_of_prod {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Fintype ι] {P : ι → X → Polynomial ℝ} (D : Delineation fun (x : Unit) (x_1 : X) => ∏ k : ι, P k x_1) {d : ι → ℕ} (hc : ∀ (k : ι), ∀ j ≤ d k, Continuous fun (x : X) => (P k x).coeff j) (hd : ∀ (k : ι) (x : X), (P k x).natDegree ≤ d k) (k : ι) (i : Fin D.count) (x y : X) : Polynomial.rootMultiplicity (D.root i x) (P k x) = Polynomial.rootMultiplicity (D.root i y) (P k y)

Along each root section of a delineated product, the multiplicity in every factor is constant on a preconnected base. Only degree bounds and continuity of coefficients through those bounds are needed; nonvanishing follows from the positive product multiplicity on the section, and no coprimality of factors is required.

noncomputable def TauCeti.Delineation.ofProd {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Fintype ι] {P : ι → X → Polynomial ℝ} (D : Delineation fun (x : Unit) (x_1 : X) => ∏ k : ι, P k x_1) [Nonempty X] (hc : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hn : ∀ (k : ι) (x : X), P k x ≠ 0) (hd : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) : Delineation P

Recover the common delineation of a finite family from a delineation of its product. The root list is unchanged, and each factor acquires its own constant multiplicities and signs. The base is nonempty so that the product's root list really enumerates roots, including when the factor family is empty.

@[simp]

theorem TauCeti.Delineation.ofProd_count {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Fintype ι] {P : ι → X → Polynomial ℝ} (D : Delineation fun (x : Unit) (x_1 : X) => ∏ k : ι, P k x_1) [Nonempty X] (hc : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hn : ∀ (k : ι) (x : X), P k x ≠ 0) (hd : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) : (D.ofProd hc hn hd).count = D.count

Passing from a product to its factors preserves the number of root sections.

@[simp]

theorem TauCeti.Delineation.ofProd_root {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Fintype ι] {P : ι → X → Polynomial ℝ} (D : Delineation fun (x : Unit) (x_1 : X) => ∏ k : ι, P k x_1) [Nonempty X] (hc : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hn : ∀ (k : ι) (x : X), P k x ≠ 0) (hd : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (i : Fin (D.ofProd hc hn hd).count) (x : X) : (D.ofProd hc hn hd).root i x = D.root (Fin.cast ⋯ i) x

Passing from a product to its factors preserves the ordered root functions.

theorem TauCeti.Delineation.ofProd_multiplicity {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Fintype ι] {P : ι → X → Polynomial ℝ} (D : Delineation fun (x : Unit) (x_1 : X) => ∏ k : ι, P k x_1) [Nonempty X] (hc : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hn : ∀ (k : ι) (x : X), P k x ≠ 0) (hd : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (k : ι) (i : Fin (D.ofProd hc hn hd).count) (x : X) : (D.ofProd hc hn hd).multiplicity k i = Polynomial.rootMultiplicity (D.root (Fin.cast ⋯ i) x) (P k x)

A factor's multiplicity in the recovered delineation is its root multiplicity along the corresponding product section, at any point of the base. Supply the point x explicitly when using this equality as a rewrite rule: the multiplicity projection does not determine a point of the base.

theorem TauCeti.Delineation.multiplicity_eq_sum_ofProd {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Fintype ι] {P : ι → X → Polynomial ℝ} (D : Delineation fun (x : Unit) (x_1 : X) => ∏ k : ι, P k x_1) [Nonempty X] (hc : ∀ (k : ι) (j : ℕ), Continuous fun (x : X) => (P k x).coeff j) (hn : ∀ (k : ι) (x : X), P k x ≠ 0) (hd : ∀ (k : ι) (x y : X), (P k x).natDegree = (P k y).natDegree) (i : Fin D.count) : D.multiplicity () i = ∑ k : ι, (D.ofProd hc hn hd).multiplicity k (Fin.cast ⋯ i)

The multiplicity of a product section is the sum of the multiplicities of that section in the factors, including when factors share roots.