Dimension of semialgebraic sets

The dimension TauCeti.semialgebraicDim s of a subset s of ℝ ^ n is the supremum of the d such that s contains a nonempty subset homeomorphic to an open subset of ℝ ^ d; the empty set has dimension ⊥. By invariance of domain this is at most n (TauCeti.semialgebraicDim_le), and a nonempty set which is itself homeomorphic to an open subset of ℝ ^ d has dimension exactly d (TauCeti.semialgebraicDim_eq_of_isOpenEmbedding).

The definition is intrinsic, and the point is that for semialgebraic sets it is computed by any cylindrical algebraic decomposition. Every cell of a CAD is locally closed (TauCeti.IsCAD.isLocallyClosed) and homeomorphic to an open subset of some ℝ ^ d (TauCeti.IsCAD.exists_injective_isOpenEmbedding_comp): a section over a base cell is homeomorphic to the base, and a sector over it is an open subset of the cylinder over the base. The dimension of a finite union of locally closed sets is the largest of their dimensions (TauCeti.semialgebraicDim_iUnion_of_isLocallyClosed), because a nonempty space covered by finitely many locally closed sets has one of them with nonempty interior. Hence the dimension of a union of cells of a CAD is the largest dimension of those cells (TauCeti.IsCAD.semialgebraicDim_eq_iSup). In particular the maximal dimension of the cells of a CAD contained in a semialgebraic set does not depend on the decomposition. Consequently the dimension of a union of two semialgebraic sets is the larger of their dimensions (TauCeti.IsSemialgebraic.semialgebraicDim_union).

Main declarations

• TauCeti.semialgebraicDim: the dimension of a subset of ℝ ^ n.
• TauCeti.semialgebraicDim_le, TauCeti.semialgebraicDim_eq_bot_iff, TauCeti.semialgebraicDim_mono: the dimension of a nonempty set lies between 0 and n, and is monotone.
• TauCeti.semialgebraicDim_le_of_isEmbedding, TauCeti.semialgebraicDim_image_of_isEmbedding: dimension is monotone along embeddings, and invariant under embeddings of the ambient space.
• TauCeti.semialgebraicDim_eq_of_isOpenEmbedding, IsOpen.semialgebraicDim_eq: a nonempty open subset of ℝ ^ d has dimension d.
• TauCeti.semialgebraicDim_iUnion_of_isLocallyClosed: dimension of finite unions of locally closed sets.
• TauCeti.IsCAD.exists_semialgebraicDim_eq: each cell of a CAD has a natural dimension d and is homeomorphic to an open subset of ℝ ^ d.
• TauCeti.IsCAD.semialgebraicDim_eq_iSup: the dimension of a union of cells of a CAD is the largest dimension of these cells.
• TauCeti.IsSemialgebraic.semialgebraicDim_union: the dimension of a union of two semialgebraic sets.
• TauCeti.IsSemialgebraic.exists_isOpenEmbedding_semialgebraicDim_eq: a nonempty semialgebraic set contains a locally closed Euclidean cell of the same dimension.

References

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

noncomputable def TauCeti.semialgebraicDim {n : ℕ} (s : Set (Fin n → ℝ)) : WithBot ℕ∞

The dimension of a subset s of ℝ ^ n: the supremum of the natural numbers d such that s contains a nonempty subset homeomorphic to an open subset of ℝ ^ d. The empty set has dimension ⊥, and every other set has a natural number dimension at most n (TauCeti.semialgebraicDim_le). For a semialgebraic set this is the largest dimension of the cells of any cylindrical algebraic decomposition adapted to it (TauCeti.IsCAD.semialgebraicDim_eq_iSup).

theorem TauCeti.semialgebraicDim_le_iff {n : ℕ} {s : Set (Fin n → ℝ)} {k : WithBot ℕ∞} : semialgebraicDim s ≤ k ↔ ∀ t ⊆ s, t.Nonempty → ∀ (d : ℕ) (f : ↑t → Fin d → ℝ), Topology.IsOpenEmbedding f → ↑d ≤ k

An upper bound for the dimension is a bound on the dimensions d of the nonempty subsets homeomorphic to open subsets of ℝ ^ d.

theorem TauCeti.le_semialgebraicDim {n : ℕ} {s : Set (Fin n → ℝ)} {X : Type u_1} [TopologicalSpace X] [Nonempty X] {g : X → Fin n → ℝ} (hg : Topology.IsEmbedding g) (hgs : Set.range g ⊆ s) {d : ℕ} {f : X → Fin d → ℝ} (hf : Topology.IsOpenEmbedding f) : ↑d ≤ semialgebraicDim s

If a nonempty space X embeds into s and has an open embedding into ℝ ^ d, then s has dimension at least d.

theorem TauCeti.semialgebraicDim_mono {n : ℕ} {s t : Set (Fin n → ℝ)} (h : s ⊆ t) : semialgebraicDim s ≤ semialgebraicDim t

Dimension is monotone.

theorem TauCeti.semialgebraicDim_le_of_isEmbedding {n : ℕ} {s : Set (Fin n → ℝ)} {m : ℕ} {t : Set (Fin m → ℝ)} {g : ↑t → Fin n → ℝ} (hg : Topology.IsEmbedding g) (hgs : Set.range g ⊆ s) : semialgebraicDim t ≤ semialgebraicDim s

Dimension is monotone along embeddings: a set which embeds into s has dimension at most that of s.

@[simp]

theorem TauCeti.semialgebraicDim_image_of_isEmbedding {n m : ℕ} {f : (Fin n → ℝ) → Fin m → ℝ} (hf : Topology.IsEmbedding f) (s : Set (Fin n → ℝ)) : semialgebraicDim (f '' s) = semialgebraicDim s

Dimension is invariant under embeddings of the ambient space.

theorem TauCeti.semialgebraicDim_le {n : ℕ} (s : Set (Fin n → ℝ)) : semialgebraicDim s ≤ ↑n

Invariance of dimension. A subset of ℝ ^ n has dimension at most n.

@[simp]

theorem TauCeti.semialgebraicDim_eq_bot_iff {n : ℕ} {s : Set (Fin n → ℝ)} : semialgebraicDim s = ⊥ ↔ s = ∅

The dimension of a set is ⊥ exactly when the set is empty.

@[simp]

theorem TauCeti.semialgebraicDim_empty {n : ℕ} : semialgebraicDim ∅ = ⊥

The empty set has dimension ⊥.

theorem TauCeti.semialgebraicDim_eq_of_isOpenEmbedding {n : ℕ} {s : Set (Fin n → ℝ)} (hs : s.Nonempty) {d : ℕ} {f : ↑s → Fin d → ℝ} (hf : Topology.IsOpenEmbedding f) : semialgebraicDim s = ↑d

A nonempty set which is homeomorphic to an open subset of ℝ ^ d has dimension d.

theorem IsOpen.semialgebraicDim_eq {n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsOpen s) (hne : s.Nonempty) : TauCeti.semialgebraicDim s = ↑n

A nonempty open subset of ℝ ^ n has dimension n.

@[simp]

theorem TauCeti.semialgebraicDim_univ {n : ℕ} : semialgebraicDim Set.univ = ↑n

The whole space ℝ ^ n has dimension n.

theorem TauCeti.semialgebraicDim_iUnion_of_isLocallyClosed {n : ℕ} {ι : Type u_1} [Finite ι] {u : ι → Set (Fin n → ℝ)} (hu : ∀ (i : ι), IsLocallyClosed (u i)) : semialgebraicDim (⋃ (i : ι), u i) = ⨆ (i : ι), semialgebraicDim (u i)

Dimension of finite unions. The dimension of a finite union of locally closed subsets of ℝ ^ n is the largest of their dimensions.

theorem TauCeti.semialgebraicDim_sUnion_of_isLocallyClosed {n : ℕ} {𝒮 : Set (Set (Fin n → ℝ))} (h𝒮 : 𝒮.Finite) (hl : ∀ u ∈ 𝒮, IsLocallyClosed u) : semialgebraicDim (⋃₀ 𝒮) = ⨆ u ∈ 𝒮, semialgebraicDim u

Dimension of finite unions. The dimension of the union of a finite family of locally closed subsets of ℝ ^ n is the largest of their dimensions.

Cells of cylindrical algebraic decompositions

theorem TauCeti.IsCAD.exists_semialgebraicDim_eq {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} {E : Set (Fin n → ℝ)} (h : IsCAD n 𝒞) (hE : E ∈ 𝒞) : ∃ (d : ℕ), semialgebraicDim E = ↑d ∧ ∃ (f : ↑E → Fin d → ℝ), Topology.IsOpenEmbedding f

Every cell E of a cylindrical algebraic decomposition has a natural number dimension d, and is homeomorphic to an open subset of ℝ ^ d.

theorem TauCeti.IsCAD.semialgebraicDim_eq_iSup {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) {s : Set (Fin n → ℝ)} (hs : ∀ E ∈ 𝒞, E ⊆ s ∨ Disjoint E s) : semialgebraicDim s = ⨆ E ∈ {E : Set (Fin n → ℝ) | E ∈ 𝒞 ∧ E ⊆ s}, semialgebraicDim E

Dimension from cells. If a set s contains or misses each cell of a cylindrical algebraic decomposition, its dimension is the largest dimension of the cells it contains. In particular this maximum does not depend on the decomposition.

theorem TauCeti.IsSemialgebraic.exists_finite_sUnion_eq {n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) : ∃ (𝒮 : Set (Set (Fin n → ℝ))), 𝒮.Finite ∧ ⋃₀ 𝒮 = s ∧ ∀ u ∈ 𝒮, IsLocallyClosed u ∧ ∃ (d : ℕ) (f : ↑u → Fin d → ℝ), Topology.IsOpenEmbedding f

A semialgebraic subset of ℝ ^ n is the union of finitely many locally closed sets, each homeomorphic to an open subset of some ℝ ^ d: the cells of an adapted cylindrical algebraic decomposition that it contains.

theorem TauCeti.IsSemialgebraic.semialgebraicDim_union {n : ℕ} {s t : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) (ht : IsSemialgebraic t) : semialgebraicDim (s ∪ t) = max (semialgebraicDim s) (semialgebraicDim t)

Dimension of unions. The dimension of the union of two semialgebraic sets is the larger of their dimensions.

theorem TauCeti.IsSemialgebraic.exists_isOpenEmbedding_semialgebraicDim_eq {n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) (hne : s.Nonempty) : ∃ u ⊆ s, IsLocallyClosed u ∧ u.Nonempty ∧ ∃ (d : ℕ), semialgebraicDim s = ↑d ∧ ∃ (f : ↑u → Fin d → ℝ), Topology.IsOpenEmbedding f

A nonempty semialgebraic set contains a locally closed subset of the same dimension which is homeomorphic to an open subset of a Euclidean space.