Analytic submanifolds in polynomial stacks

Every sector of a continuous ordered stack over a d-dimensional real analytic submanifold is an analytic submanifold of dimension d + 1. Only continuity of the boundaries is needed: the sector is relatively open in the ambient cylinder. This includes the two unbounded sectors and the whole cylinder of a stack without sections.

Together with the analytic section theorem, this proves that every cell of a delineation with intrinsically analytic coefficients has dimension either d or d + 1 and is an analytic submanifold. These are the bases needed for successive analytic polynomial liftings.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268 (analytic delineability and lifting).

theorem TauCeti.isAnalyticSubmanifold_image_cylinder_sectorSet {n d k : ℕ} {S : Set (Fin n → ℝ)} {θ : Fin k → ↑S → ℝ} (hS : IsAnalyticSubmanifold d S) (hc : ∀ (i : Fin k), Continuous (θ i)) (hθ : ∀ (x : ↑S), StrictMono fun (i : Fin k) => θ i x) (j : Fin (k + 1)) : IsAnalyticSubmanifold (d + 1) (cylinder S '' sectorSet θ j)

Every sector of a continuous strictly ordered stack over an analytic submanifold is an analytic submanifold of dimension one more than its base. No analyticity of the boundary functions is required.

theorem TauCeti.Delineation.exists_isAnalyticSubmanifold_of_mem_stackCells {n d : ℕ} {S : Set (Fin n → ℝ)} {ι : Type u_1} {P : ι → (Fin n → ℝ) → Polynomial ℝ} (D : Delineation fun (i : ι) (x : ↑S) => P i ↑x) (hS : IsAnalyticSubmanifold d S) (hcoeff : ∀ (i : ι) (j : ℕ), AnalyticOnSubmanifold d (fun (x : Fin n → ℝ) => (P i x).coeff j) S) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ stackCells S D.root) : ∃ (e : ℕ), (e = d ∨ e = d + 1) ∧ IsAnalyticSubmanifold e E

Every cell of a delineation with intrinsically analytic coefficients over a d-dimensional analytic submanifold is an analytic submanifold. Sections have dimension d, while sectors have dimension d + 1.