Changing the base of a cylindrical stack

Pulling a stack back along a map of its base pulls every section and sector back along the corresponding map of the cylinder, leaving the distinguished coordinate unchanged. Polynomial base maps, and restriction to a semialgebraic subset of the base, preserve semialgebraic stacks. When the base map is a coordinate permutation, analyticity of the ambient cells is preserved as well.

These results transport the geometric output of polynomial lifting between coordinate orders. They do not assert that arbitrary coordinate permutations preserve cylindrical decompositions, or that Lazard valuations are invariant under coordinate permutations.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 5.3.

theorem TauCeti.IsSemialgebraicStack.comp {n m k : ℕ} {C : Set (Fin n → ℝ)} {θ : Fin k → ↑C → ℝ} (hθ : IsSemialgebraicStack C θ) (p : Fin n → MvPolynomial (Fin m) ℝ) : IsSemialgebraicStack ((fun (x : Fin m → ℝ) (i : Fin n) => (MvPolynomial.eval x) (p i)) ⁻¹' C) fun (i : Fin k) (x : ↑((fun (x : Fin m → ℝ) (i : Fin n) => (MvPolynomial.eval x) (p i)) ⁻¹' C)) => θ i ⟨fun (j : Fin n) => (MvPolynomial.eval ↑x) (p j), ⋯⟩

A polynomial change of base preserves semialgebraic stacks. This uses only inverse images, not closure of semialgebraic sets under projection.

theorem TauCeti.IsSemialgebraicStack.restrict {n k : ℕ} {C D : Set (Fin n → ℝ)} {θ : Fin k → ↑C → ℝ} (hθ : IsSemialgebraicStack C θ) (hD : IsSemialgebraic D) (h : D ⊆ C) : IsSemialgebraicStack D fun (i : Fin k) => θ i ∘ Set.inclusion h

Restricting a semialgebraic stack over C to a semialgebraic subset D ⊆ C gives a semialgebraic stack over D. Its cells are the parts of the original cells lying over D (TauCeti.stackCells_inclusion).

theorem TauCeti.IsSemialgebraicStack.reindex {n k : ℕ} {C : Set (Fin n → ℝ)} {θ : Fin k → ↑C → ℝ} (hθ : IsSemialgebraicStack C θ) (e : Equiv.Perm (Fin n)) (ha : ∀ E ∈ stackCells C θ, ∃ (d : ℕ), IsAnalyticSubmanifold d E) : (IsSemialgebraicStack ((fun (x : Fin n → ℝ) => x ∘ ⇑e) ⁻¹' C) fun (i : Fin k) (x : ↑((fun (x : Fin n → ℝ) => x ∘ ⇑e) ⁻¹' C)) => θ i ⟨↑x ∘ ⇑e, ⋯⟩) ∧ ∀ E ∈ stackCells ((fun (x : Fin n → ℝ) => x ∘ ⇑e) ⁻¹' C) fun (i : Fin k) (x : ↑((fun (x : Fin n → ℝ) => x ∘ ⇑e) ⁻¹' C)) => θ i ⟨↑x ∘ ⇑e, ⋯⟩, ∃ (d : ℕ), IsAnalyticSubmanifold d E

Reordering only the base coordinates preserves a semialgebraic stack and analyticity of its cells. The newly lifted coordinate remains first.