Conjugation of analytic branches across the distinguished hyperplane

A complete, distinct analytic splitting on a punctured product extends to the full product with a unique involutive permutation of its labels implementing complex conjugation. The extended roots may collide on the hyperplane. Coefficient symmetry is required only off the hyperplane, where it determines the permutation uniquely; continuity carries the resulting branch identities through the collisions.

The parameter involution can conjugate several base coordinates. The distinguished domain can be any open conjugation-invariant complex set whose punctured part is preconnected, in particular a disc centered at zero. The coefficient tuple describes a monic polynomial and only needs continuity on the full product. The given punctured branches can be obtained after a power substitution; this theorem constructs their analytic extensions together with their conjugation action.

The construction combines exists_analyticOnNhd_monicOfCoeff_eq_prod_X_sub_C with TauCeti.existsUnique_root_conj_perm_of_subset_closure, reusing the conjugation permutation of a distinct root labelling and the analytic hyperplane extension.

Fixed labels give real branches at every parameter fixed by the involution, including on the hyperplane. The converse requires distinctness and therefore is asserted only off the hyperplane by TauCeti.root_conj_perm_apply_eq_self_iff_im_eq_zero.

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, §4.

theorem TauCeti.Polynomial.exists_analyticOnNhd_monicOfCoeff_eq_prod_X_sub_C_conj {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {U : Set V} {s : Set ℂ} {d : ℕ} {τ : V → V} (c : V × ℂ → Fin d → ℂ) (r : Fin d → V × ℂ → ℂ) (hU : IsOpen U) (hUc : IsPreconnected U) (hs : IsOpen s) (hsc : IsPreconnected (s \ {0})) (hconj : Set.MapsTo (⇑(starRingEnd ℂ)) s s) (hτ : ContinuousOn τ U) (hτU : Set.MapsTo τ U U) (hττ : ∀ x ∈ U, τ (τ x) = x) (hc : ContinuousOn c (U ×ˢ s)) (hr : ∀ (i : Fin d), AnalyticOnNhd ℂ (r i) (U ×ˢ (s \ {0}))) (hinj : ∀ p ∈ U ×ˢ (s \ {0}), Function.Injective fun (i : Fin d) => r i p) (hfac : ∀ p ∈ U ×ˢ (s \ {0}), monicOfCoeff (c p) = ∏ i : Fin d, (Polynomial.X - Polynomial.C (r i p))) (hcconj : ∀ p ∈ U ×ˢ (s \ {0}), ∀ (i : Fin d), c (τ p.1, (starRingEnd ℂ) p.2) i = (starRingEnd ℂ) (c p i)) (p₀ : V × ℂ) (hp₀ : p₀ ∈ U ×ˢ (s \ {0})) : ∃ (g : Fin d → V × ℂ → ℂ), (∀ (i : Fin d), AnalyticOnNhd ℂ (g i) (U ×ˢ s) ∧ Set.EqOn (g i) (r i) (U ×ˢ (s \ {0}))) ∧ (∀ p ∈ U ×ˢ s, monicOfCoeff (c p) = ∏ i : Fin d, (Polynomial.X - Polynomial.C (g i p))) ∧ ∃! σ : Equiv.Perm (Fin d), Function.Involutive ⇑σ ∧ ∀ (i : Fin d), ∀ p ∈ U ×ˢ s, g (σ i) p = (starRingEnd ℂ) (g i (τ p.1, (starRingEnd ℂ) p.2))

Extend a distinct punctured analytic splitting across t = 0 together with its unique conjugation permutation. The branches may coincide at t = 0; neither distinctness nor separability is required there. Symmetry of the lower coefficients is enough to determine the action on all the extended branches.