Global delineations from analytic chart coordinates

A delineation constructed on an open set of the free coordinates of an analytic chart transfers to an open neighborhood in the submanifold. Quantities constant along its root sections transfer with it. Such chart-local stacks glue over a preconnected submanifold to a global delineation carrying the same sectionwise constancy.

This connects local polynomial root constructions along analytic parametrizations to global stacks on their base. For example, take the section quantity to be the ambient order of a multivariate polynomial at Fin.cons t x: the gluing conclusion is then constancy of ambient order along each global section, rather than constancy of the order of a restricted function. The chart-coordinate open sets need not be connected, and no global root labelling or common root count is assumed.

References

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

theorem TauCeti.IsAnalyticChart.exists_delineation_of_const_on_sections {n d : ℕ} {S : Set (Fin n → ℝ)} {ι : Type u_1} {α : Type u_2} {P : ι → (Fin n → ℝ) → Polynomial ℝ} {q : (Fin n → ℝ) → ℝ → α} {e : OpenPartialHomeomorph (Fin n → ℝ) (Fin n → ℝ)} (he : IsAnalyticChart d S e) {x : Fin n → ℝ} (hx : x ∈ S) (hxe : x ∈ e.source) {V : Set (Fin d → ℝ)} (hV : IsOpen V) (hxV : (firstCoords ℝ n d) (↑e x) ∈ V) (D : Delineation fun (k : ι) (u : ↑V) => P k (↑e.symm ((firstCoords ℝ d n) ↑u))) (hq : ∀ (i : Fin D.count) (u v : ↑V), q (↑e.symm ((firstCoords ℝ d n) ↑u)) (D.root i u) = q (↑e.symm ((firstCoords ℝ d n) ↑v)) (D.root i v)) : ∃ (U : Set ↑S), IsOpen U ∧ ⟨x, hx⟩ ∈ 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)

A stack in the free coordinates of an analytic chart transfers to an open neighborhood in the base, preserving quantities constant along each section.

theorem TauCeti.exists_delineation_of_locally_chart {n d : ℕ} {S : Set (Fin n → ℝ)} {ι : Type u_1} {α : Type u_2} {P : ι → (Fin n → ℝ) → Polynomial ℝ} {q : (Fin n → ℝ) → ℝ → α} (hS : IsPreconnected S) (hlocal : ∀ x ∈ S, ∃ (e : OpenPartialHomeomorph (Fin n → ℝ) (Fin n → ℝ)), IsAnalyticChart d S e ∧ x ∈ e.source ∧ ∃ (V : Set (Fin d → ℝ)), IsOpen V ∧ (firstCoords ℝ n d) (↑e x) ∈ V ∧ ∃ (D : Delineation fun (k : ι) (u : ↑V) => P k (↑e.symm ((firstCoords ℝ d n) ↑u))), ∀ (i : Fin D.count) (u v : ↑V), q (↑e.symm ((firstCoords ℝ d n) ↑u)) (D.root i u) = q (↑e.symm ((firstCoords ℝ d n) ↑v)) (D.root i v)) : ∃ (D : Delineation fun (k : ι) (x : ↑S) => P k ↑x), ∀ (i : Fin D.count) (x y : ↑S), q (↑x) (D.root i x) = q (↑y) (D.root i y)

Delineations in analytic chart coordinates glue over a preconnected base, preserving quantities constant along their sections. The root counts and the constants may vary between the chart-local constructions; the conclusion identifies and globalizes them.

For ambient polynomial order, instantiate q with fun x t ↦ p.orderAt (Fin.cons t x). No regularity of q, finiteness of the family, or coefficient continuity is required.