Ramified splittings and real roots from constant discriminant order

A monic polynomial with real polynomial coefficients, restricted along a real analytic parametrization, admits a local analytic complex splitting after a ramified transverse substitution when its discriminant has constant finite ambient order along the parametrization. The complexification, transverse direction, branches and discriminant unit are constructed from the real data. Neither a prepared discriminant nor a splitting is assumed.

The branches retain repeated labels on the exceptional hyperplane. Their restrictions there give complex roots, even when the central fiber has multiple roots. Selecting the real branches gives a local strictly ordered analytic enumeration of the real roots of the fibers, with constant positive multiplicities.

The real root enumeration does not need monicity: it holds whenever the central fiber is nonzero and the fibers have constant degree, even if the formal leading coefficient vanishes. Translate the root coordinate to a nonroot τ of the central fiber and reverse at the formal degree. The leading coefficient becomes the value at τ, which is nonzero near the center. The integral normalization is then a monic polynomial over the same coefficient ring, and its discriminant differs from the original one by a power of that value (Polynomial.discr_integralNormalization_reverse_comp_X_add_C), so it has the same ambient order. The monic case applies to it, and undoing normalization, reversal and translation recovers the roots of the original fibers. None of these results assert constancy of the ambient order of the original polynomial on the root sections.

Main results

• Polynomial.exists_analyticAt_prod_X_sub_C_of_orderAt_discr_eq: a monic family splits into analytic factors after a ramified transverse substitution, in every direction of an open dense set.
• Polynomial.exists_analyticOnNhd_ordered_roots_of_orderAt_discr_eq: the real roots of a family with nonzero central fiber and constant fiber degree have a local ordered analytic enumeration with constant multiplicities.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998).
• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Section 4.

theorem Polynomial.exists_analyticAt_prod_X_sub_C_of_orderAt_discr_eq {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Fintype ι] (p : Polynomial (MvPolynomial σ ℝ)) (hp : p.Monic) {φ : (ι → ℝ) → σ → ℝ} {a : ι → ℝ} {m : ℕ} (hφ : AnalyticAt ℝ φ a) (hm : ∀ᶠ (x : ι → ℝ) in nhds a, p.discr.orderAt (φ x) = ↑m) : ∃ (Φ : (ι → ℂ) → σ → ℂ) (V : Set (σ → ℝ)), IsOpen V ∧ Dense V ∧ (AnalyticAt ℂ Φ fun (j : ι) => ↑(a j)) ∧ (∀ᶠ (x : ι → ℝ) in nhds a, (Φ fun (j : ι) => ↑(x j)) = fun (i : σ) => ↑(φ x i)) ∧ ∀ v ∈ V, ∃ (r : Fin p.natDegree → (ι → ℂ) × ℂ → ℂ) (u : (ι → ℂ) × ℂ → ℂ), (∀ (i : Fin p.natDegree), AnalyticAt ℂ (r i) (fun (j : ι) => ↑(a j), 0)) ∧ AnalyticAt ℂ u (fun (j : ι) => ↑(a j), 0) ∧ u (fun (j : ι) => ↑(a j), 0) ≠ 0 ∧ ∀ᶠ (z : (ι → ℂ) × ℂ) in nhds (fun (j : ι) => ↑(a j), 0), map (MvPolynomial.eval₂Hom Complex.ofRealHom (Φ z.1 + z.2 ^ p.natDegree.factorial • fun (i : σ) => ↑(v i))) p = ∏ i : Fin p.natDegree, (X - C (r i z)) ∧ (map (MvPolynomial.eval₂Hom Complex.ofRealHom (Φ z.1 + z.2 ^ p.natDegree.factorial • fun (i : σ) => ↑(v i))) p).discr = z.2 ^ (p.natDegree.factorial * m) * u z

Constant finite ambient order of the formal discriminant along a real analytic parametrization produces complex analytic splittings after transverse power substitutions. The complexification of the parametrization is shared, and every real direction in an open dense set gives such a splitting. The ramification exponent is the factorial of the formal degree. The constructed discriminant unit is nonzero at the center; root labels may collide on the exceptional hyperplane.

theorem Polynomial.exists_analyticOnNhd_ordered_roots_of_orderAt_discr_eq {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Fintype ι] (p : Polynomial (MvPolynomial σ ℝ)) {φ : (ι → ℝ) → σ → ℝ} {a : ι → ℝ} {d m : ℕ} (hφ : AnalyticAt ℝ φ a) (hp : map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ a)) p ≠ 0) (hd : ∀ᶠ (x : ι → ℝ) in nhds a, (map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ x)) p).natDegree = d) (hm : ∀ᶠ (x : ι → ℝ) in nhds a, p.discr.orderAt (φ x) = ↑m) : ∃ (k : ℕ) (s : Fin k → (ι → ℝ) → ℝ) (U : Set (ι → ℝ)), IsOpen U ∧ a ∈ U ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (s i) U) ∧ (∀ x ∈ U, StrictMono fun (i : Fin k) => s i x) ∧ (∀ x ∈ U, ∀ (t : ℝ), (map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ x)) p).IsRoot t ↔ ∃ (i : Fin k), s i x = t) ∧ (∀ (i : Fin k), 0 < rootMultiplicity (s i a) (map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ a)) p)) ∧ ∀ x ∈ U, ∀ (i : Fin k), rootMultiplicity (s i x) (map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ x)) p) = rootMultiplicity (s i a) (map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ a)) p)

Local analytic roots from constant discriminant order. Let p be a polynomial whose coefficients are real polynomials, specialized along a real analytic parametrization φ. If the fiber at a is nonzero, the fibers near a have constant degree, and the formal discriminant of p has constant finite ambient order near a, then the real roots of the fibers near a have a strictly ordered analytic enumeration with constant positive multiplicities.

The formal leading coefficient of p may vanish at a, so the degree of the fibers can be smaller than the formal degree at which the discriminant is taken.