Conjugation-compatible Laurent forms of nonmonic roots

The Laurent forms extracted from an analytic splitting of integral normalization respect a conjugation action on the original roots: conjugate labels have equal integer exponents and conjugate analytic units. The unit identity holds across the exceptional hyperplane, even when the original roots have poles there.

Root branches, their analytic scaled extensions, and the action on labels are inputs. Neither Laurent exponents nor unit symmetry are assumed. This permits the root-covering and conjugation arguments to be used independently of the extraction of Laurent units. No simplicity assumption is needed for this step.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), §4, Corollary 4.2.

theorem TauCeti.exists_root_eq_zpow_mul_unit_conj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d a c : ℕ} (hd : 0 < d) {P : E × ℂ → Polynomial ℂ} {r s : Fin d → E × ℂ → ℂ} {x₀ : E} {u v : E × ℂ → ℂ} (hs : ∀ (i : Fin d), AnalyticAt ℂ (s i) (x₀, 0)) (hu : AnalyticAt ℂ u (x₀, 0)) (hu0 : u (x₀, 0) ≠ 0) (hv : AnalyticAt ℂ v (x₀, 0)) (hv0 : v (x₀, 0) ≠ 0) (hnorm : ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), p.2 ≠ 0 → (P p).integralNormalization = ∏ i : Fin d, (Polynomial.X - Polynomial.C (s i p))) (hlead : ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), (P p).coeff d = p.2 ^ c * v p) (hconst : ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), (P p).coeff 0 = p.2 ^ a * u p) (hscale : ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), p.2 ≠ 0 → ∀ (i : Fin d), (P p).coeff d * r i p = s i p) {τ : E → E} (hτ : ContinuousAt τ x₀) (hτ0 : τ x₀ = x₀) {σ : Fin d → Fin d} (hσ : ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), p.2 ≠ 0 → ∀ (i : Fin d), r (σ i) p = (starRingEnd ℂ) (r i (τ p.1, (starRingEnd ℂ) p.2))) : ∃ (e : Fin d → ℤ) (w : Fin d → E × ℂ → ℂ), (∀ (i : Fin d), AnalyticAt ℂ (w i) (x₀, 0)) ∧ (∀ (i : Fin d), w i (x₀, 0) ≠ 0) ∧ (∀ (i : Fin d), e (σ i) = e i) ∧ ∀ᶠ (p : E × ℂ) in nhds (x₀, 0), (∀ (i : Fin d), w i p ≠ 0) ∧ (∀ (i : Fin d), w (σ i) p = (starRingEnd ℂ) (w i (τ p.1, (starRingEnd ℂ) p.2))) ∧ (p.2 ≠ 0 → ∀ (i : Fin d), r i p = p.2 ^ e i * w i p)

Laurent forms of nonmonic roots can be chosen compatibly with conjugation. The parameter map is continuous at and fixes the central parameter; the distinguished coordinate is conjugated. Labels related by σ have the same Laurent exponent, and their unit germs satisfy the corresponding conjugation identity on the full neighborhood. The root equations themselves are required only off the hyperplane, where poles are allowed.