Multiplicities along continuous polynomial sections

For a coefficientwise continuous family of locally bounded degree, multiplicity at a continuous point is locally bounded above by its central value, provided the central polynomial is nonzero. Hasse derivatives give this statement in arbitrary characteristic. Over an integral domain, if each factor is nonzero at the base point and the multiplicity in a finite product is locally constant, every factor multiplicity is locally constant: none can increase, and their sum cannot decrease.

This transfers the multiplicities of root sections of a product to its individual factors, including factors sharing roots and roots of multiplicity greater than one.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Section 2 (delineability of a polynomial basis).

theorem Polynomial.continuousAt_hasseDeriv_eval {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [TopologicalSpace R] {r : B → R} {x₀ : B} {d : ℕ} [Semiring R] [IsTopologicalSemiring R] {F : B → Polynomial R} (m : ℕ) (hF : ∀ (i : ℕ), m ≤ i → i ≤ d → ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : B) in nhds x₀, (F x).natDegree ≤ d) (hr : ContinuousAt r x₀) : ContinuousAt (fun (x : B) => eval (r x) ((hasseDeriv m) (F x))) x₀

Evaluation of a Hasse derivative along a point continuous at x₀ is continuous at x₀ for a family whose coefficients of indices from m through d are continuous at x₀ and whose degrees are bounded by d near x₀. Coefficients below m do not affect the derivative.

theorem Polynomial.eventually_rootMultiplicity_le {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [TopologicalSpace R] {r : B → R} {x₀ : B} {d : ℕ} [CommRing R] [IsTopologicalSemiring R] {F : B → Polynomial R} [T1Space R] (hF : ∀ i ≤ d, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : B) in nhds x₀, (F x).natDegree ≤ d) (hr : ContinuousAt r x₀) (hne : F x₀ ≠ 0) : ∀ᶠ (x : B) in nhds x₀, rootMultiplicity (r x) (F x) ≤ rootMultiplicity (r x₀) (F x₀)

Multiplicity at a continuous point cannot increase nearby when the central polynomial is nonzero. Zero nearby polynomials are allowed, with their usual multiplicity zero.

theorem Polynomial.eventually_rootMultiplicity_eq_of_prod {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [TopologicalSpace R] {r : B → R} {x₀ : B} [CommRing R] [IsTopologicalSemiring R] [IsDomain R] [T1Space R] {ι : Type u_3} {F : ι → B → Polynomial R} {d : ι → ℕ} (s : Finset ι) (hF : ∀ k ∈ s, ∀ i ≤ d k, ContinuousAt (fun (x : B) => (F k x).coeff i) x₀) (hdeg : ∀ k ∈ s, ∀ᶠ (x : B) in nhds x₀, (F k x).natDegree ≤ d k) (hr : ContinuousAt r x₀) (hne : ∀ k ∈ s, F k x₀ ≠ 0) (hmult : ∀ᶠ (x : B) in nhds x₀, rootMultiplicity (r x) (∏ k ∈ s, F k x) = rootMultiplicity (r x₀) (∏ k ∈ s, F k x₀)) : ∀ᶠ (x : B) in nhds x₀, ∀ k ∈ s, rootMultiplicity (r x) (F k x) = rootMultiplicity (r x₀) (F k x₀)

Along a continuous point, locally constant multiplicity in a nonzero finite product forces locally constant multiplicity in every factor. No coprimality is required.

theorem TauCeti.Polynomial.rootMultiplicity_eq_of_prod {B : Type u_1} {R : Type u_2} {ι : Type u_3} [TopologicalSpace B] [PreconnectedSpace B] [TopologicalSpace R] [CommRing R] [IsTopologicalSemiring R] [IsDomain R] [T1Space R] {F : ι → B → Polynomial R} {r : B → R} {d : ι → ℕ} (s : Finset ι) (hF : ∀ k ∈ s, ∀ i ≤ d k, Continuous fun (x : B) => (F k x).coeff i) (hdeg : ∀ k ∈ s, ∀ (x : B), (F k x).natDegree ≤ d k) (hr : Continuous r) (hne : ∀ k ∈ s, ∀ (x : B), F k x ≠ 0) (hmult : ∀ (x y : B), Polynomial.rootMultiplicity (r x) (∏ k ∈ s, F k x) = Polynomial.rootMultiplicity (r y) (∏ k ∈ s, F k y)) (k : ι) (hk : k ∈ s) (x y : B) : Polynomial.rootMultiplicity (r x) (F k x) = Polynomial.rootMultiplicity (r y) (F k y)

Constant multiplicity along a continuous point in a nonzero finite product forces constant multiplicity in each factor on a preconnected base. Only degree bounds are needed; the factors need not be coprime.