Documentation

TauCeti.Geometry.RealAlgebraic.CAD.McCallum.Basic

Order-invariant cylindrical algebraic decompositions by McCallum projection #

McCallum's projection replaces the Collins projection by the contents, coefficients, discriminants and pairwise resultants of a squarefree basis (Finset.mcCallumProjection). It is correct under a well-orientedness assumption, and it then produces a cylindrical algebraic decomposition whose cells are analytic submanifolds and on whose cells every input polynomial is order-invariant: its ambient order of vanishing MvPolynomial.orderAt is constant on each cell. Order-invariance implies sign-invariance on connected cells (IsPreconnected.signInvariant_eval_of_orderAt_eq).

The lifting step works with any squarefree, pairwise relatively prime primitive basis. It takes a CAD of ℝ ^ n with analytic submanifold cells, on which the McCallum projection of the family is order-invariant. Over a cell with more than one point, no basis polynomial may be nullified; the cell then carries a common delineation of the basis (Finset.IsSquarefreeBasis.exists_delineation_orderAt_eq_of_mcCallumProjection). Over a single point, basis polynomials may be nullified, and the line over the point is refined by the roots of the delineating polynomials of the inputs (Finset.exists_isSemialgebraicStack_orderAt_eq). In both cases every input is order-invariant on the resulting cells, which are again analytic submanifolds.

The hypothesis excluding nullification over cells with more than one point cannot be dropped (TauCeti.exists_nullified_mcCallumProjection_orderAt_ne). Over the line x₁ = x₂ = 0 of ℝ ^ 3, the polynomial X₂ (X₀ + 1) + X₃ X₁ is nullified, while its McCallum projection is order-invariant. Above the line its order is one except at the single point (-1, 0, 0, 0), where it is at least two. Every cell of a stack lies over the whole line, so no stack over the line makes it order-invariant. This is the failure condition of McCallum's lifting.

A finite family is well-oriented in McCallum's sense (TauCeti.IsMcCallumWellOriented) when, at every level of the recursive projection, it has a squarefree basis each of whose members is nullified at only finitely many points. On a cell where the projection is order-invariant, a basis polynomial nullified at one point is nullified on the whole cell, because the projection contains its coefficients. A connected cell inside a finite set is a point, so over a cell with more than one point no basis polynomial is nullified, and the lifting step applies at every level. Every family of polynomials in at most two variables is well-oriented.

Main definitions and results #

References #

source
theorem TauCeti.exists_isSemialgebraicStack_orderAt_eq_of_mcCallumProjection {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F : Finset (MvPolynomial (Fin (n + 1)) ℝ)} {B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} (hB : (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).IsSquarefreeBasis B) {C : Set (Fin n → ℝ)} {d : ℕ} (hC : IsSemialgebraic C) (hCa : IsAnalyticSubmanifold d C) (hconn : IsPreconnected C) (hproj : ∀ q ∈ (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).mcCallumProjection B, ∀ x ∈ C, ∀ y ∈ C, q.orderAt x = q.orderAt y) (hfiber : C.Nontrivial → ∀ b ∈ B, ∀ x ∈ C, Polynomial.map (MvPolynomial.eval x) b ≠ 0) :
∃ (k : ℕ) (θ : Fin k → ↑C → ℝ), IsSemialgebraicStack C θ ∧ ∀ E ∈ stackCells C θ, (∃ (e : ℕ), IsAnalyticSubmanifold e E) ∧ ∀ f ∈ F, ∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y'

McCallum lifting over one cell. Let B be a squarefree basis of a finite family F of real polynomials in n + 1 variables, with the distinguished variable X 0 singled out, and let C ⊆ ℝ ^ n be a semialgebraic, preconnected analytic submanifold on which every element of the McCallum projection is order-invariant. If no member of B is nullified over C whenever C has more than one point, then there is a semialgebraic stack over C whose cells are analytic submanifolds, on each of which every member of F is order-invariant.

source
theorem TauCeti.IsCAD.exists_isCAD_orderAt_eq_of_mcCallumProjection {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F : Finset (MvPolynomial (Fin (n + 1)) ℝ)} {B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {𝒟 : Set (Set (Fin n → ℝ))} (h𝒟 : IsCAD n 𝒟) (hB : (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).IsSquarefreeBasis B) (hanalytic : ∀ C ∈ 𝒟, ∃ (d : ℕ), IsAnalyticSubmanifold d C) (hproj : ∀ q ∈ (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).mcCallumProjection B, ∀ C ∈ 𝒟, ∀ x ∈ C, ∀ y ∈ C, q.orderAt x = q.orderAt y) (hfiber : ∀ C ∈ 𝒟, C.Nontrivial → ∀ b ∈ B, ∀ x ∈ C, Polynomial.map (MvPolynomial.eval x) b ≠ 0) :
∃ (𝒞 : Set (Set (Fin (n + 1) → ℝ))), IsCAD (n + 1) 𝒞 ∧ Set.image Fin.tail '' 𝒞 = 𝒟 ∧ (∀ E ∈ 𝒞, ∃ (d : ℕ), IsAnalyticSubmanifold d E) ∧ ∀ f ∈ F, ∀ E ∈ 𝒞, ∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y'

McCallum lifting of a cylindrical algebraic decomposition. Let B be a squarefree basis of a finite family F of real polynomials in n + 1 variables, with the distinguished variable X 0 singled out. Let 𝒟 be a CAD of ℝ ^ n into analytic submanifolds, on whose cells every element of the McCallum projection is order-invariant, such that no member of B is nullified over a cell with more than one point. Then 𝒟 lifts to a CAD of ℝ ^ (n + 1) into analytic submanifolds, on whose cells every member of F is order-invariant.

Nullification over cells with more than one point #

source
theorem TauCeti.exists_nullified_mcCallumProjection_orderAt_ne (polynomialGCD : NormalizedGCDMonoid (MvPolynomial (Fin 3) ℝ)) :
have this := polynomialGCD; ∃ (f : MvPolynomial (Fin 4) ℝ) (C : Set (Fin 3 → ℝ)), IsSemialgebraic C ∧ IsAnalyticSubmanifold 1 C ∧ IsConnected C ∧ ∀ (B : Finset (Polynomial (MvPolynomial (Fin 3) ℝ))), (Finset.map (MvPolynomial.finSuccEquiv ℝ 3).toEmbedding {f}).IsIrreducibleBasis B → (∀ q ∈ (Finset.map (MvPolynomial.finSuccEquiv ℝ 3).toEmbedding {f}).mcCallumProjection B, ∀ x ∈ C, ∀ y ∈ C, q.orderAt x = q.orderAt y) ∧ (∀ b ∈ B, ∀ x ∈ C, Polynomial.map (MvPolynomial.eval x) b = 0) ∧ ∀ (k : ℕ) (θ : Fin k → ↑C → ℝ), (∀ (x : ↑C), StrictMono fun (i : Fin k) => θ i x) → ∃ E ∈ stackCells C θ, ∃ y ∈ E, ∃ y' ∈ E, f.orderAt y ≠ f.orderAt y'

McCallum lifting fails over positive-dimensional nullifying cells. The hypothesis of TauCeti.exists_isSemialgebraicStack_orderAt_eq_of_mcCallumProjection that no basis member is nullified over a cell with more than one point cannot be dropped, even over a connected semialgebraic analytic submanifold on which the McCallum projection is order-invariant.

Explicitly, let f = X₂ (X₀ + 1) + X₃ X₁, a polynomial in the distinguished variable X₀ and the base coordinates X₁, X₂, X₃, and let C ⊆ ℝ ^ 3 be the line of base points x with x₁ = x₂ = 0. As a polynomial in X₀, f is linear with coprime coefficients X₂ and X₂ + X₃ X₁, each of which vanishes to order one at every point of C; its content and discriminant are units. So for every irreducible basis B of {f}, every element of the McCallum projection has constant order on C, while every member of B is nullified over C. But f has order at least two at the point (-1, 0, 0, 0) above C, and order one at every point above C where X₀ ≠ -1 or X₁ ≠ 0. Since every cell of a stack over C lies over the whole of C, no stack over C, given by pointwise strictly increasing functions, continuous or not, has f order-invariant on each cell.

Well-oriented families #

source
def TauCeti.IsMcCallumWellOriented (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) (n : ℕ) :
Finset (MvPolynomial (Fin n) ℝ) → Prop

A finite family F of real polynomials in n variables is well-oriented in McCallum's sense if, when n is positive, singling out the distinguished variable X 0 gives a family with a squarefree basis B such that each member of B is nullified at only finitely many points of ℝ ^ (n - 1), and the McCallum projection of the family with respect to B is again well-oriented. Every family of constants is well-oriented.

Instances For
    source
    @[simp]
    theorem TauCeti.isMcCallumWellOriented_zero (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) (F : Finset (MvPolynomial (Fin 0) ℝ)) :
    IsMcCallumWellOriented polynomialGCD 0 F

    Every family of polynomials in no variables is well-oriented.

    source
    theorem TauCeti.isMcCallumWellOriented_succ_iff {n : ℕ} (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) {F : Finset (MvPolynomial (Fin (n + 1)) ℝ)} :
    IsMcCallumWellOriented polynomialGCD (n + 1) F ↔ ∃ (B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))), (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).IsSquarefreeBasis B ∧ (∀ b ∈ B, {x : Fin n → ℝ | Polynomial.map (MvPolynomial.eval x) b = 0}.Finite) ∧ IsMcCallumWellOriented polynomialGCD n ((Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).mcCallumProjection B)

    A family of polynomials in n + 1 variables is well-oriented exactly when it has a squarefree basis in the distinguished variable X 0 whose members are nullified at finitely many points, and whose McCallum projection is well-oriented.

    source
    @[simp]
    theorem TauCeti.isMcCallumWellOriented_one (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) (F : Finset (MvPolynomial (Fin 1) ℝ)) :
    IsMcCallumWellOriented polynomialGCD 1 F

    Every family of polynomials in one variable is well-oriented: its basis polynomials are nullified at most at the single point of ℝ ^ 0.

    source
    @[simp]
    theorem TauCeti.isMcCallumWellOriented_two (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) (F : Finset (MvPolynomial (Fin 2) ℝ)) :
    IsMcCallumWellOriented polynomialGCD 2 F

    Every family of polynomials in two variables is well-oriented: a basis polynomial is nonzero, so it has a nonzero coefficient, a polynomial in one variable with finitely many zeros.

    source
    theorem TauCeti.exists_isCAD_orderAt_eq_of_isMcCallumWellOriented {n : ℕ} (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) {F : Finset (MvPolynomial (Fin n) ℝ)} (hF : IsMcCallumWellOriented polynomialGCD n F) :
    ∃ (𝒞 : Set (Set (Fin n → ℝ))), IsCAD n 𝒞 ∧ (∀ E ∈ 𝒞, ∃ (d : ℕ), IsAnalyticSubmanifold d E) ∧ ∀ f ∈ F, ∀ E ∈ 𝒞, ∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y'

    Correctness of McCallum's projection. A finite family of real polynomials that is well-oriented in McCallum's sense has a cylindrical algebraic decomposition into analytic submanifolds, on each cell of which every member of the family has constant ambient order.