Gluing local delineations

Local delineations of a real polynomial family glue over a preconnected base. The ordered real roots have no permutation ambiguity on overlaps, so their number, multiplicities, and the degrees and nullification status of the family members are constant. The resulting continuous root functions form one global delineation. No finiteness assumption on the family or continuity assumption on its coefficients is needed: local delineations already provide finite root lists and local sign-invariance.

The gluing of the ordered root lists uses TauCeti.exists_roots_of_locally from the earlier real-root API. It applies to local continuous increasing enumerations of any intrinsic root set, so it also glues the root functions of local Lazard delineations.

This gives the passage from local analytic root constructions to a global stack. Analyticity of its root functions can then be obtained from the analytic root-section API.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268 (globalization of local delineability).

theorem TauCeti.nonempty_delineation_of_locally {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [PreconnectedSpace X] (hlocal : ∀ (x : X), ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ Nonempty (Delineation fun (k : ι) (y : ↑U) => P k ↑y)) : Nonempty (Delineation P)

A family with a delineation on a neighborhood of every point has a global delineation on any preconnected base. Local root counts, multiplicities, degrees, nullification and signs are allowed to depend on the neighborhood; their global constancy is a conclusion.