Dimension of semialgebraic sets under coordinate projections

A change of coordinates x ↦ x ∘ ι, for any ι : Fin m → Fin n and in particular for a coordinate projection, does not increase the dimension of a semialgebraic subset of ℝ ^ n (TauCeti.IsSemialgebraic.semialgebraicDim_image_comp_le). For the projection Fin.tail forgetting coordinate 0 this is read off a cylindrical algebraic decomposition adapted to the set: each of its cells contains the graph of a continuous function over the projected cell, so the projected cell embeds into the cell. When ι is surjective, x ↦ x ∘ ι is an embedding of the ambient space and preserves dimension; otherwise it is a coordinate permutation, followed by forgetting coordinate 0, followed by a change of coordinates with one coordinate fewer. Without semialgebraicity the bound fails: the graph of the indicator function of the rationals contains no arc, so it has dimension 0, but it projects onto ℝ.

Conversely, every cell of such a decomposition is mapped homeomorphically onto an open subset of ℝ ^ d by a projection onto d of its coordinates. Together these give a characterization of dimension by coordinate projections (TauCeti.IsSemialgebraic.natCast_le_semialgebraicDim_iff): a semialgebraic set has dimension at least d exactly when some projection onto d distinct coordinates maps it onto a set with nonempty interior.

Main declarations

• TauCeti.semialgebraicDim_image_comp_of_surjective: changes of coordinates x ↦ x ∘ ι with ι surjective, such as coordinate permutations, preserve dimension.
• TauCeti.IsSemialgebraic.semialgebraicDim_image_tail_le, TauCeti.IsSemialgebraic.semialgebraicDim_image_comp_le: coordinate projections do not increase the dimension of semialgebraic sets.
• TauCeti.IsSemialgebraic.natCast_le_semialgebraicDim_iff: dimension by coordinate projections with nonempty interior.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Ergebnisse der Mathematik und ihrer Grenzgebiete 36, Springer, 1998, Section 2.8.

@[simp]

theorem TauCeti.semialgebraicDim_image_comp_of_surjective {m n : ℕ} {ι : Fin m → Fin n} (hι : Function.Surjective ι) (s : Set (Fin n → ℝ)) : semialgebraicDim ((fun (x : Fin n → ℝ) => x ∘ ι) '' s) = semialgebraicDim s

A change of coordinates x ↦ x ∘ ι with ι surjective, such as a coordinate permutation, does not change the dimension: it embeds ℝ ^ n into ℝ ^ m.

theorem TauCeti.IsSemialgebraic.semialgebraicDim_image_tail_le {n : ℕ} {s : Set (Fin (n + 1) → ℝ)} (hs : IsSemialgebraic s) : semialgebraicDim (Fin.tail '' s) ≤ semialgebraicDim s

Projection does not increase dimension. Forgetting coordinate 0 does not increase the dimension of a semialgebraic set.

theorem TauCeti.IsSemialgebraic.semialgebraicDim_image_comp_le {m n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) (ι : Fin m → Fin n) : semialgebraicDim ((fun (x : Fin n → ℝ) => x ∘ ι) '' s) ≤ semialgebraicDim s

Coordinate projections do not increase dimension. For every ι : Fin m → Fin n, the image of a semialgebraic set under x ↦ x ∘ ι has at most its dimension.

theorem TauCeti.IsSemialgebraic.natCast_le_semialgebraicDim_iff {n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) {d : ℕ} : ↑d ≤ semialgebraicDim s ↔ ∃ (ι : Fin d → Fin n), Function.Injective ι ∧ (interior ((fun (x : Fin n → ℝ) => x ∘ ι) '' s)).Nonempty

Dimension by coordinate projections. A semialgebraic subset of ℝ ^ n has dimension at least d exactly when its projection x ↦ x ∘ ι onto some d distinct coordinates has nonempty interior in ℝ ^ d.