Gluing constant data on root sections

Suppose a real polynomial family admits local delineations, and a quantity is constant along each section of each local stack. Then the quantity is locally constant along every section of any global delineation. Over a preconnected base it is constant along each global section, and the local stacks themselves glue to a global delineation.

The quantity may take values in any type, with no topology. In particular, it can be the ambient polynomial order at a section point. Its values on sectors are unconstrained. Root labels need no identification in the hypotheses: increasing complete root lists identify the sections on overlaps. Neither finiteness of the polynomial family nor continuity of its coefficients is required.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268, Sections 2–3 (order-invariance and globalization of delineability).

theorem TauCeti.Delineation.isLocallyConstant_root_of_locally {X : Type u_1} {ι : Type u_2} {α : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : Delineation P) (q : X → ℝ → α) (hlocal : ∀ (x : X), ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ ∃ (D' : Delineation fun (k : ι) (y : ↑U) => P k ↑y), ∀ (i : Fin D'.count) (y z : ↑U), q (↑y) (D'.root i y) = q (↑z) (D'.root i z)) (i : Fin D.count) : IsLocallyConstant fun (x : X) => q x (D.root i x)

If a quantity is constant on the sections of local delineations around every point, it is locally constant on the sections of any global delineation. No agreement of local labels is assumed.

theorem TauCeti.exists_delineation_of_locally_const_on_sections {X : Type u_1} {ι : Type u_2} {α : Type u_3} [TopologicalSpace X] {P : ι → X → Polynomial ℝ} [PreconnectedSpace X] (q : X → ℝ → α) (hlocal : ∀ (x : X), ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ ∃ (D : Delineation fun (k : ι) (y : ↑U) => P k ↑y), ∀ (i : Fin D.count) (y z : ↑U), q (↑y) (D.root i y) = q (↑z) (D.root i z)) : ∃ (D : Delineation P), ∀ (i : Fin D.count) (x y : X), q x (D.root i x) = q y (D.root i y)

Local delineations carrying quantities constant along their sections glue over a preconnected base to a global delineation with those quantities constant along its sections. The constants, root counts, and local root labels may depend on the neighborhood.