Documentation

TauCeti.Geometry.RealAlgebraic.Projection.Integer

The Collins projection of integer families #

A finite family P of polynomials with integer coefficients in the variables X 0, …, X n enters cylindrical decomposition over ℝ by mapping its coefficients to ℝ and singling out the distinguished variable X 0 with MvPolynomial.finSuccEquiv. This gives the real family P.integerFamily of polynomials in X 0 over ℝ[X 1, …, X n], whose fibers over a point x of ℝⁿ are the univariate polynomials t ↦ f (Fin.cons t x), f ∈ P (MvPolynomial.polynomial_eval_map_finSuccEquiv).

The Collins projection of this real family can be computed without leaving the integers: single out X 0 over ℤ and project there. The result P.integerProjection is a finite family of integer polynomials in n variables. The injective map Int.castRingHom ℝ preserves the degrees of all reducta and of their derivatives, so the principal subresultant coefficients are taken at the same formal bounds over ℤ and over ℝ, and the image of the integer projection is exactly the Collins projection of the real family. Hence sign conditions on the integer projection delineate the real family.

Main definitions #

Main results #

References #

source
noncomputable def Finset.integerFamily {n : ℕ} (P : Finset (MvPolynomial (Fin (n + 1)) ℤ)) :
Finset (Polynomial (MvPolynomial (Fin n) ℝ))

The real family attached to a finite family P of integer polynomials in the variables X 0, …, X n: map the coefficients to ℝ and single out the distinguished variable X 0.

Instances For
    source
    noncomputable def Finset.integerProjection {n : ℕ} (P : Finset (MvPolynomial (Fin (n + 1)) ℤ)) :
    Finset (MvPolynomial (Fin n) ℤ)

    The Collins projection of a finite family P of integer polynomials in the variables X 0, …, X n, computed over ℤ: single out the distinguished variable X 0 and take the Collins projection of the resulting family of polynomials in X 0 over ℤ[X 1, …, X n].

    Instances For
      source
      @[simp]
      theorem Finset.mem_integerFamily {n : ℕ} {P : Finset (MvPolynomial (Fin (n + 1)) ℤ)} {g : Polynomial (MvPolynomial (Fin n) ℝ)} :
      g ∈ P.integerFamily ↔ ∃ f ∈ P, (MvPolynomial.finSuccEquiv ℝ n) ((MvPolynomial.map (Int.castRingHom ℝ)) f) = g

      The members of the real family of P are the members of P mapped to ℝ, with the distinguished variable X 0 singled out.

      source
      theorem Finset.integerProjection_def {n : ℕ} (P : Finset (MvPolynomial (Fin (n + 1)) ℤ)) :
      P.integerProjection = (image (⇑(MvPolynomial.finSuccEquiv ℤ n)) P).collinsProjection

      The integer projection is the Collins projection of the family obtained by singling out the distinguished variable X 0 over ℤ.

      source
      @[simp]
      theorem Finset.integerFamily_empty {n : ℕ} :
      ∅.integerFamily = ∅

      The real family of the empty family is empty.

      source
      @[simp]
      theorem Finset.integerProjection_empty {n : ℕ} :
      ∅.integerProjection = ∅

      The integer projection of the empty family is empty.

      source
      theorem Finset.integerFamily_mono {n : ℕ} {P Q : Finset (MvPolynomial (Fin (n + 1)) ℤ)} (h : P ⊆ Q) :
      P.integerFamily ⊆ Q.integerFamily

      Enlarging a family of integer polynomials enlarges its real family.

      source
      theorem Finset.integerProjection_mono {n : ℕ} {P Q : Finset (MvPolynomial (Fin (n + 1)) ℤ)} (h : P ⊆ Q) :
      P.integerProjection ⊆ Q.integerProjection

      Enlarging a family of integer polynomials enlarges its integer projection.

      source
      theorem Finset.image_map_integerProjection {n : ℕ} [DecidableEq (MvPolynomial (Fin n) ℝ)] (P : Finset (MvPolynomial (Fin (n + 1)) ℤ)) :
      image (⇑(MvPolynomial.map (Int.castRingHom ℝ))) P.integerProjection = P.integerFamily.collinsProjection

      The integer projection computes the real projection. Mapping the integer projection of P to ℝ gives the Collins projection of the real family of P.

      source
      theorem TauCeti.nonempty_delineation_integerFamily_of_signInvariant_integerProjection {n : ℕ} {S : Set (Fin n → ℝ)} {P : Finset (MvPolynomial (Fin (n + 1)) ℤ)} (hS : IsPreconnected S) (h : ∀ q ∈ P.integerProjection, SignInvariant (fun (x : Fin n → ℝ) => MvPolynomial.eval₂ (Int.castRingHom ℝ) x q) S) :
      Nonempty (Delineation fun (p : ↥P.integerFamily) (x : ↑S) => Polynomial.map (MvPolynomial.eval₂Hom (RingHom.id ℝ) ↑x) ↑p)

      Integer delineability. Let P be a finite family of polynomials with integer coefficients in the variables X 0, …, X n. If every element of its integer projection is sign-invariant on a preconnected set S ⊆ ℝⁿ, then the real family of P has a delineation over S: its fibers over x ∈ S are the polynomials t ↦ f (Fin.cons t x), f ∈ P.