Cylindrical algebraic decompositions

A cylindrical algebraic decomposition (CAD) of ℝ ^ n is a finite partition of ℝ ^ n into semialgebraic cells, built one dimension at a time. The only CAD of ℝ ^ 0 is the partition into the single point. A CAD of ℝ ^ (n + 1) is obtained from a CAD of ℝ ^ n by choosing, over each of its cells C, finitely many continuous functions θ₀ < θ₁ < … < θₖ₋₁ : C → ℝ whose sections and sectors are semialgebraic, and taking all the sections and sectors of all these stacks. The distinguished new coordinate is coordinate 0, as for TauCeti.cylinder.

TauCeti.IsCAD n 𝒞 is this recursive definition, for a set 𝒞 of subsets of Fin n → ℝ. The cells are not assumed to be connected, nor the decomposition to be a partition: these are theorems. Every cell of a CAD is a nonempty, connected, semialgebraic set, there are finitely many cells, and they partition ℝ ^ n. Each cell is locally closed and is mapped homeomorphically onto an open subset of some ℝ ^ d by a coordinate projection: a section is homeomorphic to the base cell below it, and a sector is open in the cylinder over its base cell. Each cell also contains the graph of a continuous function on its projection. The projections of the cells of a CAD of ℝ ^ (n + 1) form a CAD of ℝ ^ n, and the decomposition is cylindrical: two cells have equal or disjoint projections, so each cell lies over the whole of the lower cell it meets.

A CAD is adapted to a family of polynomials when each of them is sign-invariant on each cell. Every set described by a condition on their signs is then a union of cells, so its projection is a union of projected cells and is semialgebraic. Every semialgebraic set is described by such a condition (TauCeti.IsSemialgebraic.exists_eq_setOf_sign_eval); together with the existence of adapted CADs this gives the closure of semialgebraic sets under projection. One sample point in each cell of an adapted CAD realizes every sign condition that the polynomials realize anywhere.

Stacks of polynomial functions are semialgebraic. In particular finitely many points of ℝ, together with the open intervals they cut out, form a CAD of ℝ ^ 1.

Main declarations

• TauCeti.IsSemialgebraicStack: a continuous, strictly ordered stack with semialgebraic cells.
• TauCeti.IsCAD: cylindrical algebraic decompositions, defined recursively.
• TauCeti.IsCAD.isPartition, TauCeti.IsCAD.finite, TauCeti.IsCAD.isSemialgebraic, TauCeti.IsCAD.isConnected: a CAD is a finite partition into connected semialgebraic cells.
• TauCeti.IsCAD.isLocallyClosed, TauCeti.IsCAD.exists_injective_isOpenEmbedding_comp: every cell is locally closed, and a coordinate projection maps it homeomorphically onto an open subset of some ℝ ^ d.
• TauCeti.IsCAD.exists_continuous_cons_mem: every cell contains the graph of a continuous function on its projection.
• TauCeti.IsCAD.injOn_tail_of_finite, TauCeti.IsCAD.isEmbedding_tail_of_injOn: finite vertical fibers force projection to be injective on a cell, and injective projection is an embedding.
• TauCeti.IsCAD.image_tail, TauCeti.IsCAD.image_tail_eq_or_disjoint: projecting a CAD gives a CAD, and projections of cells are equal or disjoint.
• TauCeti.IsCAD.sUnion_sep_subset: a set containing or missing each cell is the union of the cells it contains.
• TauCeti.IsCAD.isSemialgebraic_image_tail, TauCeti.IsCAD.isSemialgebraic_image_tail_setOf_sign_eval: projections of unions of cells, in particular of sign-condition sets of polynomials sign-invariant on the cells, are semialgebraic.
• TauCeti.IsCAD.exists_finite_image_sign_eval_eq: sample points of an adapted CAD realize all sign conditions.
• TauCeti.isSemialgebraicStack_eval, TauCeti.isCAD_stackCells_const: polynomial stacks, and the CAD of ℝ ^ 1 cut out by finitely many points.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 5.1 (cylindrical algebraic decomposition).

Semialgebraic stacks

structure TauCeti.IsSemialgebraicStack {n k : ℕ} (C : Set (Fin n → ℝ)) (θ : Fin k → ↑C → ℝ) : Prop

A semialgebraic stack over C ⊆ ℝ ^ n: finitely many continuous functions θ₀ < θ₁ < … < θₖ₋₁ on C whose sections and sectors, placed in ℝ ^ (n + 1) by TauCeti.cylinder, are semialgebraic. These are the stacks from which a cylindrical algebraic decomposition is built.

• continuous (i : Fin k) : Continuous (θ i)

  Each function of the stack is continuous.

• strictMono (x : ↑C) : StrictMono fun (i : Fin k) => θ i x

  The functions of the stack are strictly ordered at each point.

• isSemialgebraic_sectionSet (i : Fin k) : IsSemialgebraic (cylinder C '' sectionSet θ i)

  Each section of the stack is semialgebraic.

• isSemialgebraic_sectorSet (j : Fin (k + 1)) : IsSemialgebraic (cylinder C '' sectorSet θ j)

  Each sector of the stack is semialgebraic.

theorem TauCeti.IsSemialgebraicStack.isSemialgebraic {n k : ℕ} {C : Set (Fin n → ℝ)} {θ : Fin k → ↑C → ℝ} (hθ : IsSemialgebraicStack C θ) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ stackCells C θ) : IsSemialgebraic E

Every cell of a semialgebraic stack is semialgebraic.

theorem TauCeti.isSemialgebraicStack_eval {n k : ℕ} {C : Set (Fin n → ℝ)} (hC : IsSemialgebraic C) (p : Fin k → MvPolynomial (Fin n) ℝ) (hp : ∀ x ∈ C, StrictMono fun (i : Fin k) => (MvPolynomial.eval x) (p i)) : IsSemialgebraicStack C fun (i : Fin k) (x : ↑C) => (MvPolynomial.eval ↑x) (p i)

A stack of polynomial functions on a semialgebraic set, strictly ordered at each point, is a semialgebraic stack.

Cylindrical algebraic decompositions

inductive TauCeti.IsCAD (n : ℕ) : Set (Set (Fin n → ℝ)) → Prop

IsCAD n 𝒞 says that the set 𝒞 of subsets of ℝ ^ n is a cylindrical algebraic decomposition of ℝ ^ n. The decomposition of ℝ ^ 0 is the single cell univ. A decomposition of ℝ ^ (n + 1) consists of all the cells of the stacks over the cells of a decomposition 𝒟 of ℝ ^ n, where over each cell C ∈ 𝒟 the stack θ C is a semialgebraic stack. The new coordinate is coordinate 0.

• zero : IsCAD 0 {Set.univ}

  The decomposition of ℝ ^ 0 into a single point.

• succ {n : ℕ} {𝒟 : Set (Set (Fin n → ℝ))} (k : Set (Fin n → ℝ) → ℕ) (θ : (C : Set (Fin n → ℝ)) → Fin (k C) → ↑C → ℝ) : IsCAD n 𝒟 → (∀ C ∈ 𝒟, IsSemialgebraicStack C (θ C)) → IsCAD (n + 1) (⋃ C ∈ 𝒟, stackCells C (θ C))

  Lift a decomposition 𝒟 of ℝ ^ n by a semialgebraic stack over each of its cells.

theorem TauCeti.IsCAD.exists_succ_of_forall_exists_stack {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h𝒞 : IsCAD n 𝒞) (P : Set (Fin (n + 1) → ℝ) → Prop) (h : ∀ C ∈ 𝒞, ∃ (k : ℕ) (θ : Fin k → ↑C → ℝ), IsSemialgebraicStack C θ ∧ ∀ E ∈ stackCells C θ, P E) : ∃ (𝒟 : Set (Set (Fin (n + 1) → ℝ))), IsCAD (n + 1) 𝒟 ∧ Set.image Fin.tail '' 𝒟 = 𝒞 ∧ ∀ E ∈ 𝒟, P E

Stacks over every cell of a CAD assemble into a CAD whose projections are exactly the original cells. Any property shared by all stack cells holds on every cell of the new CAD.

theorem TauCeti.IsCAD.finite {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) : 𝒞.Finite

A cylindrical algebraic decomposition has finitely many cells.

theorem TauCeti.IsCAD.isSemialgebraic {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) {E : Set (Fin n → ℝ)} (hE : E ∈ 𝒞) : IsSemialgebraic E

Every cell of a cylindrical algebraic decomposition is semialgebraic.

theorem TauCeti.IsCAD.isConnected {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) {E : Set (Fin n → ℝ)} (hE : E ∈ 𝒞) : IsConnected E

Every cell of a cylindrical algebraic decomposition is connected, and in particular nonempty.

theorem TauCeti.IsCAD.isLocallyClosed {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) {E : Set (Fin n → ℝ)} (hE : E ∈ 𝒞) : IsLocallyClosed E

Every cell of a cylindrical algebraic decomposition is locally closed.

theorem TauCeti.IsCAD.exists_injective_isOpenEmbedding_comp {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) {E : Set (Fin n → ℝ)} (hE : E ∈ 𝒞) : ∃ (d : ℕ) (ι : Fin d → Fin n), Function.Injective ι ∧ Topology.IsOpenEmbedding fun (x : ↑E) => ↑x ∘ ι

Every cell E of a cylindrical algebraic decomposition of ℝ ^ n is mapped homeomorphically onto an open subset of some ℝ ^ d by a coordinate projection x ↦ x ∘ ι, with ι : Fin d → Fin n injective. A section of a stack is projected like its base cell, since it is the graph of a continuous function on that cell; a sector is open in the cylinder over its base cell, and its projection also keeps the new coordinate 0.

theorem TauCeti.IsCAD.exists_continuous_cons_mem {n : ℕ} {𝒞 : Set (Set (Fin (n + 1) → ℝ))} (h : IsCAD (n + 1) 𝒞) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ 𝒞) : ∃ (g : ↑(Fin.tail '' E) → ℝ), Continuous g ∧ ∀ (x : ↑(Fin.tail '' E)), Fin.cons (g x) ↑x ∈ E

Every cell of a cylindrical algebraic decomposition of ℝ ^ (n + 1) contains the graph of a continuous function on its projection Fin.tail '' E: a section is such a graph, and a sector contains one.

theorem TauCeti.IsCAD.injOn_tail_of_finite {n : ℕ} {𝒞 : Set (Set (Fin (n + 1) → ℝ))} (h : IsCAD (n + 1) 𝒞) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ 𝒞) (hfin : ∀ (x : Fin n → ℝ), {t : ℝ | Fin.cons t x ∈ E}.Finite) : Set.InjOn Fin.tail E

A cylindrical cell with finite vertical fibers has injective vertical projection.

theorem TauCeti.IsCAD.isEmbedding_tail_of_injOn {n : ℕ} {𝒞 : Set (Set (Fin (n + 1) → ℝ))} (h : IsCAD (n + 1) 𝒞) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ 𝒞) (hinj : Set.InjOn Fin.tail E) : Topology.IsEmbedding fun (x : ↑E) => Fin.tail ↑x

Projection is a topological embedding on a cylindrical cell whenever it is injective there. The continuous section supplied by the stack is its inverse on the projected cell.

theorem TauCeti.IsCAD.isPartition {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) : Setoid.IsPartition 𝒞

The cells of a cylindrical algebraic decomposition of ℝ ^ n partition ℝ ^ n.

theorem TauCeti.IsCAD.image_tail {n : ℕ} {𝒞 : Set (Set (Fin (n + 1) → ℝ))} (h : IsCAD (n + 1) 𝒞) : IsCAD n (Set.image Fin.tail '' 𝒞)

The projections of the cells of a cylindrical algebraic decomposition of ℝ ^ (n + 1), forgetting the distinguished coordinate 0, form a cylindrical algebraic decomposition of ℝ ^ n.

theorem TauCeti.IsCAD.image_tail_eq_or_disjoint {n : ℕ} {𝒞 : Set (Set (Fin (n + 1) → ℝ))} (h : IsCAD (n + 1) 𝒞) {E E' : Set (Fin (n + 1) → ℝ)} (hE : E ∈ 𝒞) (hE' : E' ∈ 𝒞) : Fin.tail '' E = Fin.tail '' E' ∨ Disjoint (Fin.tail '' E) (Fin.tail '' E')

A cylindrical algebraic decomposition is cylindrical: the projections of two of its cells are equal or disjoint.

Decompositions adapted to sign conditions

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

A set containing or missing each cell of a cylindrical algebraic decomposition is the union of the cells it contains.

theorem TauCeti.IsCAD.isSemialgebraic_image_tail {n : ℕ} {𝒞 : Set (Set (Fin (n + 1) → ℝ))} (h : IsCAD (n + 1) 𝒞) {s : Set (Fin (n + 1) → ℝ)} (hs : ∀ E ∈ 𝒞, E ⊆ s ∨ Disjoint E s) : IsSemialgebraic (Fin.tail '' s)

Projections of unions of cells. If a set s ⊆ ℝ ^ (n + 1) contains or misses each cell of a cylindrical algebraic decomposition, then its projection forgetting coordinate 0 is semialgebraic: it is the union of the projections of the cells contained in s, which are cells of the projected decomposition.

theorem TauCeti.IsCAD.isSemialgebraic_image_tail_setOf_sign_eval {n : ℕ} {𝒞 : Set (Set (Fin (n + 1) → ℝ))} (h : IsCAD (n + 1) 𝒞) {ι : Type u_1} {p : ι → MvPolynomial (Fin (n + 1)) ℝ} (hp : ∀ (i : ι), ∀ E ∈ 𝒞, SignInvariant (fun (x : Fin (n + 1) → ℝ) => (MvPolynomial.eval x) (p i)) E) (Φ : (ι → SignType) → Prop) : IsSemialgebraic (Fin.tail '' {x : Fin (n + 1) → ℝ | Φ fun (i : ι) => SignType.sign ((MvPolynomial.eval x) (p i))})

If the polynomials p i are sign-invariant on each cell of a cylindrical algebraic decomposition of ℝ ^ (n + 1), then the projection forgetting coordinate 0 of any set described by a condition on the signs of the p i is semialgebraic.

theorem TauCeti.IsCAD.exists_finite_image_sign_eval_eq {n : ℕ} {𝒞 : Set (Set (Fin n → ℝ))} (h : IsCAD n 𝒞) {ι : Type u_1} {p : ι → MvPolynomial (Fin n) ℝ} (hp : ∀ (i : ι), ∀ E ∈ 𝒞, SignInvariant (fun (x : Fin n → ℝ) => (MvPolynomial.eval x) (p i)) E) : ∃ (T : Set (Fin n → ℝ)), T.Finite ∧ (∀ E ∈ 𝒞, ∃ (x : Fin n → ℝ), E ∩ T = {x}) ∧ (fun (x : Fin n → ℝ) (i : ι) => SignType.sign ((MvPolynomial.eval x) (p i))) '' T = Set.range fun (x : Fin n → ℝ) (i : ι) => SignType.sign ((MvPolynomial.eval x) (p i))

Sample points. If the polynomials p i are sign-invariant on each cell of a cylindrical algebraic decomposition of ℝ ^ n, there is a finite set T of sample points, exactly one in each cell, at which the p i take exactly the sign vectors that they take on ℝ ^ n.

theorem TauCeti.isCAD_singleton_univ (n : ℕ) : IsCAD n {Set.univ}

The trivial cylindrical algebraic decomposition of ℝ ^ n into a single cell.

theorem TauCeti.isCAD_stackCells_const {k : ℕ} {c : Fin k → ℝ} (hc : StrictMono c) : IsCAD 1 (stackCells Set.univ fun (i : Fin k) (x : ↑Set.univ) => c i)

Strictly increasing points c₀ < c₁ < … < cₖ₋₁ of ℝ, together with the open intervals they cut out, form a cylindrical algebraic decomposition of ℝ ^ 1.