Conjugation of continuous polynomial root branches

Suppose a polynomial family on a connected parameter space has a continuous labelling of all its roots, pointwise distinct, and its coefficients intertwine a continuous involution of the parameters with complex conjugation. Conjugation then acts on the labels by one unique involutive permutation, independent of the parameter. At any parameter fixed by the involution, a branch is real precisely when its label is fixed by this permutation. In particular a branch which is real at one fixed parameter is real at every fixed parameter.

For Puiseux branches, the parameter involution conjugates the complex base coordinates and the power-substitution variable. The punctured product is connected and the roots are distinct there. The conclusions concern the given branches; their construction and their extension across the missing hyperplane are separate results.

existsUnique_root_conj_perm_of_subset_closure extends this permutation to a larger parameter set on which the branches are continuous. Distinctness is needed only on the preconnected dense subset; roots may collide on its boundary.

For real polynomial families, persistence of collisions also gives a local realness criterion without distinctness: a labelled root is real nearby exactly when it is real at the center.

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.

theorem TauCeti.eventually_root_im_eq_zero_iff_of_persistent_collisions {B : Type u_1} {ι : Type u_2} [TopologicalSpace B] [Finite ι] {F : B → Polynomial ℝ} {r : ι → B → ℂ} {b₀ : B} (hr : ∀ (i : ι), ContinuousAt (r i) b₀) (hroot : ∀ᶠ (b : B) in nhds b₀, ∀ (z : ℂ), (Polynomial.map (algebraMap ℝ ℂ) (F b)).IsRoot z ↔ ∃ (i : ι), r i b = z) (hcollision : ∀ (i j : ι), r j b₀ = r i b₀ → r j =ᶠ[nhds b₀] r i) : ∀ᶠ (b : B) in nhds b₀, ∀ (i : ι), (r i b).im = 0 ↔ (r i b₀).im = 0

In a finite continuous complete labelling of the complex roots of a real polynomial family, the real labels are locally constant if collisions persist locally. Repeated labels are allowed, and neither connectedness nor coefficient continuity is required.

theorem TauCeti.existsUnique_root_conj_perm {B : Type u_1} {ι : Type u_2} [TopologicalSpace B] [PreconnectedSpace B] [Finite ι] {F : B → Polynomial ℂ} {r : ι → B → ℂ} {τ : B → B} (hr : ∀ (i : ι), Continuous (r i)) (hinj : ∀ (b : B), Function.Injective fun (i : ι) => r i b) (hroot : ∀ (b : B) (z : ℂ), (F b).IsRoot z ↔ ∃ (i : ι), r i b = z) (hτ : Continuous τ) (hττ : Function.Involutive τ) (hF : ∀ (b : B), F (τ b) = Polynomial.map (starRingEnd ℂ) (F b)) (b₀ : B) : ∃! σ : Equiv.Perm ι, Function.Involutive ⇑σ ∧ ∀ (i : ι) (b : B), r (σ i) b = (starRingEnd ℂ) (r i (τ b))

Conjugation acts on a continuous, pointwise distinct complete labelling of the roots by a unique permutation, and that permutation is an involution. The coefficient symmetry is expressed by mapping the polynomial by complex conjugation; no analyticity or monicity is required.

theorem TauCeti.root_conj_perm_apply_eq_self_iff_im_eq_zero {B : Type u_1} {ι : Type u_2} {r : ι → B → ℂ} {b : B} (hinj : Function.Injective fun (i : ι) => r i b) {σ : Equiv.Perm ι} (hσ : ∀ (i : ι), r (σ i) b = (starRingEnd ℂ) (r i b)) (i : ι) : σ i = i ↔ (r i b).im = 0

For a distinct root labelling on which conjugation acts by a permutation, a root is real exactly when its label is fixed by that permutation. This is a pointwise criterion.

theorem TauCeti.root_im_eq_zero_iff_of_fixed {B : Type u_1} {ι : Type u_2} [TopologicalSpace B] [PreconnectedSpace B] [Finite ι] {F : B → Polynomial ℂ} {r : ι → B → ℂ} {τ : B → B} (hr : ∀ (i : ι), Continuous (r i)) (hinj : ∀ (b : B), Function.Injective fun (i : ι) => r i b) (hroot : ∀ (b : B) (z : ℂ), (F b).IsRoot z ↔ ∃ (i : ι), r i b = z) (hτ : Continuous τ) (hττ : Function.Involutive τ) (hF : ∀ (b : B), F (τ b) = Polynomial.map (starRingEnd ℂ) (F b)) {b₀ b₁ : B} (hb₀ : τ b₀ = b₀) (hb₁ : τ b₁ = b₁) (i : ι) : (r i b₀).im = 0 ↔ (r i b₁).im = 0

A branch real at one conjugation-fixed parameter is real at every conjugation-fixed parameter, even when the fixed locus itself is disconnected.

theorem TauCeti.existsUnique_root_conj_perm_of_subset_closure {B : Type u_1} {ι : Type u_2} [TopologicalSpace B] [Finite ι] {S T : Set B} {F : B → Polynomial ℂ} {r : ι → B → ℂ} {τ : B → B} (hS : IsPreconnected S) (hST : S ⊆ T) (hTS : T ⊆ closure S) (hr : ∀ (i : ι), ContinuousOn (r i) T) (hinj : ∀ b ∈ S, Function.Injective fun (i : ι) => r i b) (hroot : ∀ b ∈ S, ∀ (z : ℂ), (F b).IsRoot z ↔ ∃ (i : ι), r i b = z) (hτ : ContinuousOn τ T) (hτS : Set.MapsTo τ S S) (hτT : Set.MapsTo τ T T) (hττ : ∀ b ∈ S, τ (τ b) = b) (hF : ∀ b ∈ S, F (τ b) = Polynomial.map (starRingEnd ℂ) (F b)) (b₀ : ↑S) : ∃! σ : Equiv.Perm ι, Function.Involutive ⇑σ ∧ ∀ (i : ι), ∀ b ∈ T, r (σ i) b = (starRingEnd ℂ) (r i (τ b))

Conjugation of a complete, distinct root labelling on a preconnected subset extends uniquely to its continuous branches on a larger set contained in its closure. Roots may collide on the larger set. Polynomial symmetry and root coverage are required only on the dense subset.