The roots of a family of separable polynomials form a covering space

Let F : B → 𝕜[X] be a family of polynomials of constant degree d over an algebraically closed RCLike field (that is, over ℂ), whose coefficients depend continuously on the parameter b. Its root space is the subtype {q : B × 𝕜 // (F q.1).IsRoot q.2} of pairs (b, z) with z a root of F b, and it comes with the projection (b, z) ↦ b. Over the parameters at which F b is separable, that is, at which its discriminant does not vanish, this projection is a covering map whose fibres have d points. No continuous labelling of all the roots exists globally in general, because of monodromy, but there is one near every separable member, and that local labelling is the even covering.

When the parameter space is a normed space and the coefficients are analytic, the sheets of the covering are analytic: a continuous function r with r x a root of F x is analytic at every point where that root is simple. This is the analytic implicit root theorem applied to (x, z) ↦ (F x).eval z, together with the uniqueness half of that theorem, which forces the continuous root r to agree with the implicit root near the point.

These are the inputs for the Puiseux theorem with parameters: a monic polynomial with analytic coefficients on U × D, whose discriminant vanishes only on U × {0}, has a root space which is a d-sheeted covering of U × (D \ {0}). Lifting a power substitution through that covering gives continuous root functions, and the analyticity statement here makes them analytic.

Main results

• TauCeti.Polynomial.analyticAt_eval_of_analyticAt_coeff: a family with analytic coefficients and locally bounded degree is analytic in the parameter and the argument jointly.
• TauCeti.Polynomial.analyticAt_of_eventually_isRoot: a continuous root of an analytic family is analytic at a point where it is a simple root.
• TauCeti.Polynomial.exists_continuousOn_isRoot_iff: near a separable member of a continuous family of constant degree, the roots can be labelled by d continuous, pairwise distinct functions.
• TauCeti.Polynomial.isEvenlyCovered_fst_isRoot: the projection from the root space is evenly covered, with fibre Fin d, near every separable member.
• TauCeti.Polynomial.isCoveringMapOn_fst_isRoot, TauCeti.Polynomial.isCoveringMap_fst_isRoot: the root space is a covering space over the separable members, and over the whole parameter space when every member is separable.
• TauCeti.Polynomial.preimageFstIsRootEquiv: the fibre of the root space over b is the set of roots of F b.
• TauCeti.Polynomial.finite_preimage_fst_isRoot, TauCeti.Polynomial.natCard_preimage_fst_isRoot: the fibre over a separable member of degree d has exactly d points.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 4 (the root covering in the Puiseux theorem with parameters).
• S. G. Krantz, H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser (2002), Chapter 2 (the analytic implicit function theorem).

Continuous roots of analytic families are analytic

theorem TauCeti.Polynomial.analyticAt_eval_of_analyticAt_coeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : E → Polynomial 𝕜} {x₀ : E} {d : ℕ} (hF : ∀ i ≤ d, AnalyticAt 𝕜 (fun (x : E) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : E) in nhds x₀, (F x).natDegree ≤ d) (z₀ : 𝕜) : AnalyticAt 𝕜 (fun (v : E × 𝕜) => Polynomial.eval v.2 (F v.1)) (x₀, z₀)

A family of polynomials whose coefficients are analytic at x₀, and whose degree stays at most d near x₀, is analytic at (x₀, z₀) as a function of the parameter and the argument jointly.

theorem TauCeti.Polynomial.analyticAt_of_eventually_isRoot {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : E → Polynomial 𝕜} {x₀ : E} {d : ℕ} [CompleteSpace 𝕜] [CompleteSpace E] (hF : ∀ i ≤ d, AnalyticAt 𝕜 (fun (x : E) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : E) in nhds x₀, (F x).natDegree ≤ d) {r : E → 𝕜} (hr : ContinuousAt r x₀) (hroot : ∀ᶠ (x : E) in nhds x₀, (F x).IsRoot (r x)) (hsimple : Polynomial.eval (r x₀) (Polynomial.derivative (F x₀)) ≠ 0) : AnalyticAt 𝕜 r x₀

A continuous root of an analytic family is analytic at a simple root. Let F be a family of polynomials with coefficients analytic at x₀ and degree at most d near x₀. If r is continuous at x₀, r x is a root of F x for all x near x₀, and r x₀ is a simple root of F x₀, then r is analytic at x₀.

In particular, the root coordinate x ↦ (s x).1.2 of a continuous local section s of the root space of such a family is analytic wherever the root it picks out is simple.

The root space of a separable family is a covering space

theorem TauCeti.Polynomial.exists_continuousOn_isRoot_iff {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {B : Type u_2} [TopologicalSpace B] {F : B → Polynomial 𝕜} {d : ℕ} (hF : ∀ i ≤ d, Continuous fun (b : B) => (F b).coeff i) (hdeg : ∀ (b : B), (F b).natDegree = d) {b₀ : B} (hsep : (F b₀).Separable) : ∃ (U : Set B), IsOpen U ∧ b₀ ∈ U ∧ ∃ (σ : Fin d → B → 𝕜), (∀ (i : Fin d), ContinuousOn (σ i) U) ∧ ∀ b ∈ U, (Function.Injective fun (i : Fin d) => σ i b) ∧ ∀ (z : 𝕜), (F b).IsRoot z ↔ ∃ (i : Fin d), σ i b = z

The roots of a separable member can be labelled continuously nearby. Let F be a family of polynomials of constant degree d with continuous coefficients. Near a parameter b₀ at which F b₀ is separable there are d continuous functions σ i, pairwise distinct at every parameter, whose values are exactly the roots of F b.

theorem TauCeti.Polynomial.isEvenlyCovered_fst_isRoot {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {B : Type u_2} [TopologicalSpace B] {F : B → Polynomial 𝕜} {d : ℕ} (hF : ∀ i ≤ d, Continuous fun (b : B) => (F b).coeff i) (hdeg : ∀ (b : B), (F b).natDegree = d) {b₀ : B} (hsep : (F b₀).Separable) : IsEvenlyCovered (fun (q : { q : B × 𝕜 // (F q.1).IsRoot q.2 }) => (↑q).1) b₀ (Fin d)

The root space is evenly covered near a separable member. For a family of polynomials of constant degree d with continuous coefficients, the projection (b, z) ↦ b from the space of pairs with z a root of F b is evenly covered, with fibre Fin d, near every parameter b₀ at which F b₀ is separable.

theorem TauCeti.Polynomial.isCoveringMapOn_fst_isRoot {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {B : Type u_2} [TopologicalSpace B] {F : B → Polynomial 𝕜} {d : ℕ} (hF : ∀ i ≤ d, Continuous fun (b : B) => (F b).coeff i) (hdeg : ∀ (b : B), (F b).natDegree = d) : IsCoveringMapOn (fun (q : { q : B × 𝕜 // (F q.1).IsRoot q.2 }) => (↑q).1) {b : B | (F b).Separable}

The root space is a covering space over the separable members. For a family of polynomials of constant degree with continuous coefficients, the projection (b, z) ↦ b from the space of pairs with z a root of F b is a covering map over the set of parameters b at which F b is separable.

theorem TauCeti.Polynomial.isCoveringMap_fst_isRoot {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {B : Type u_2} [TopologicalSpace B] {F : B → Polynomial 𝕜} {d : ℕ} (hF : ∀ i ≤ d, Continuous fun (b : B) => (F b).coeff i) (hdeg : ∀ (b : B), (F b).natDegree = d) (hsep : ∀ (b : B), (F b).Separable) : IsCoveringMap fun (q : { q : B × 𝕜 // (F q.1).IsRoot q.2 }) => (↑q).1

The root space of a separable family is a covering space. For a family of separable polynomials of constant degree with continuous coefficients, for instance a family of monic polynomials whose discriminant vanishes nowhere, the projection (b, z) ↦ b from the space of pairs with z a root of F b is a covering map.

The fibres of the root space

def TauCeti.Polynomial.preimageFstIsRootEquiv {K : Type u_1} [CommRing K] {B : Type u_2} (F : B → Polynomial K) (b : B) : ↑((fun (q : { q : B × K // (F q.1).IsRoot q.2 }) => (↑q).1) ⁻¹' {b}) ≃ { z : K // (F b).IsRoot z }

The fibre of the root space over b is the set of roots of F b: a point (b, z) of the fibre corresponds to the root z.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Polynomial.preimageFstIsRootEquiv_apply_coe {K : Type u_1} [CommRing K] {B : Type u_2} (F : B → Polynomial K) (b : B) (q : ↑((fun (q : { q : B × K // (F q.1).IsRoot q.2 }) => (↑q).1) ⁻¹' {b})) : ↑((preimageFstIsRootEquiv F b) q) = (↑↑q).2

@[simp]

theorem TauCeti.Polynomial.preimageFstIsRootEquiv_symm_apply_coe_coe {K : Type u_1} [CommRing K] {B : Type u_2} (F : B → Polynomial K) (b : B) (z : { z : K // (F b).IsRoot z }) : ↑↑((preimageFstIsRootEquiv F b).symm z) = (b, ↑z)

theorem TauCeti.Polynomial.finite_preimage_fst_isRoot {K : Type u_1} [CommRing K] [IsDomain K] {B : Type u_2} {F : B → Polynomial K} {b : B} (hb : F b ≠ 0) : Finite ↑((fun (q : { q : B × K // (F q.1).IsRoot q.2 }) => (↑q).1) ⁻¹' {b})

The fibre of the root space over a parameter b with F b ≠ 0 is finite.

theorem TauCeti.Polynomial.natCard_preimage_fst_isRoot {B : Type u_2} {K : Type u_3} [Field K] [IsAlgClosed K] {F : B → Polynomial K} {b : B} {d : ℕ} (hdeg : (F b).natDegree = d) (hsep : (F b).Separable) : Nat.card ↑((fun (q : { q : B × K // (F q.1).IsRoot q.2 }) => (↑q).1) ⁻¹' {b}) = d

The fibre of the root space over a parameter b at which F b is separable of degree d has exactly d points, over an algebraically closed field.