Finite fibers and semialgebraic dimension

A semialgebraic function with finite fibers on its domain preserves dimension, without any continuity assumption. The fibers need not have a common cardinality, and the function need not be injective. This is the zero-dimensional-fiber case of the semialgebraic fiber-dimension theorem; in particular, semialgebraic bijections preserve dimension.

The key observation is that a cylindrical cell has order-connected vertical fibers. If these are finite, they contain at most one point. The continuous section of the cell's projection therefore parametrizes the whole cell, so projection is an embedding on each cell of an adapted decomposition. Finite unions then give the dimension equality, and iteration handles arbitrary coordinate projections. Applying this to the two projections of a semialgebraic graph gives the result for arbitrary semialgebraic functions.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Section 2.8.

theorem TauCeti.IsSemialgebraic.semialgebraicDim_image_tail_of_finite {n : ℕ} {s : Set (Fin (n + 1) → ℝ)} (hs : IsSemialgebraic s) (hfin : ∀ (x : Fin n → ℝ), {t : ℝ | Fin.cons t x ∈ s}.Finite) : semialgebraicDim (Fin.tail '' s) = semialgebraicDim s

Forgetting one coordinate preserves the dimension of a semialgebraic set if every vertical fiber is finite. Empty sets and empty fibers are allowed.

theorem TauCeti.IsSemialgebraic.semialgebraicDim_image_comp_of_finite {m n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) (ι : Fin m → Fin n) (hfin : ∀ (y : Fin m → ℝ), {x : Fin n → ℝ | x ∈ s ∧ x ∘ ι = y}.Finite) : semialgebraicDim ((fun (x : Fin n → ℝ) => x ∘ ι) '' s) = semialgebraicDim s

Finite-fiber dimension theorem for coordinate projections. A coordinate projection with finite fibers on a semialgebraic set preserves dimension. Coordinates may be repeated or reordered, and no uniform bound on the finite fibers is required.

theorem TauCeti.IsSemialgebraicOn.semialgebraicDim_image_of_finite {m n : ℕ} {s : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → Fin m → ℝ} (hf : IsSemialgebraicOn f s) (hfin : ∀ (y : Fin m → ℝ), {x : Fin n → ℝ | x ∈ s ∧ f x = y}.Finite) : semialgebraicDim (f '' s) = semialgebraicDim s

Finite-fiber dimension theorem. A semialgebraic function with finite fibers on its domain preserves dimension. In particular this applies to semialgebraic bijections, without requiring continuity of the function or its inverse.