Complex polynomial equations in real coordinates

A complex polynomial equation in complex coordinates z and their conjugates star z becomes two real polynomial equations, its real and imaginary parts, in the real coordinates Re z and Im z. So the subsets of complex coordinate spaces cut out by such equations are semialgebraic once complex coordinates are split into their real and imaginary parts. This is how complex algebraic sets, and sets such as the Hermitian matrices that also involve conjugation, enter real algebraic geometry.

The real coordinates of z : κ → ℂ are indexed by κ ⊕ κ: Sum.inl k is the real part and Sum.inr k the imaginary part of z k, as in TauCeti.complexToRealEuclidean.

Main results

• TauCeti.isSemialgebraic_setOf_eval_ofReal_eq_zero: the real points of a complex polynomial equation form a semialgebraic set.
• TauCeti.isSemialgebraic_setOf_eval_sumElim_star_eq_zero: the zero set of a polynomial in complex coordinates and their conjugates is semialgebraic in the real coordinates.
• TauCeti.isSemialgebraicOn_complexToRealPi_of_forall_eq_iff: a map between complex coordinate spaces whose graph is cut out by such equations is semialgebraic in the real coordinates.

theorem TauCeti.isSemialgebraic_setOf_eval_ofReal_eq_zero {σ : Type u_1} (r : MvPolynomial σ ℂ) : IsSemialgebraic {a : σ → ℝ | (MvPolynomial.eval fun (s : σ) => ↑(a s)) r = 0}

The real points a : σ → ℝ of a complex polynomial equation r(a) = 0 form a semialgebraic set: it is cut out by the real polynomials whose coefficients are the real and the imaginary parts of the coefficients of r.

theorem TauCeti.isSemialgebraic_setOf_eval_sumElim_star_eq_zero {κ : Type u_2} (q : MvPolynomial (κ ⊕ κ) ℂ) : IsSemialgebraic {a : κ ⊕ κ → ℝ | (MvPolynomial.eval (Sum.elim (fun (k : κ) => ↑(a (Sum.inl k)) + ↑(a (Sum.inr k)) * Complex.I) fun (k : κ) => star (↑(a (Sum.inl k)) + ↑(a (Sum.inr k)) * Complex.I))) q = 0}

The zero set of a polynomial q(z, star z) in complex coordinates z : κ → ℂ and their conjugates is semialgebraic in the real coordinates a : κ ⊕ κ → ℝ, where z k = a (Sum.inl k) + a (Sum.inr k) * I.

theorem TauCeti.isSemialgebraicOn_complexToRealPi_of_forall_eq_iff {σ : Type u_3} {τ : Type u_4} {ι : Type u_5} [Fintype σ] [Fintype τ] [Finite ι] {g : (σ → ℂ) → τ → ℂ} {s : Set (σ → ℂ)} (hs : IsSemialgebraic (⇑(complexToRealPi σ).symm ⁻¹' s)) (R : ι → MvPolynomial ((σ ⊕ τ) ⊕ σ ⊕ τ) ℂ) (hR : ∀ z ∈ s, ∀ (w : τ → ℂ), g z = w ↔ ∀ (k : ι), (MvPolynomial.eval (Sum.elim (Sum.elim z w) fun (t : σ ⊕ τ) => star (Sum.elim z w t))) (R k) = 0) : IsSemialgebraicOn (fun (a : σ ⊕ σ → ℝ) => (complexToRealPi τ) (g ((complexToRealPi σ).symm a))) (⇑(complexToRealPi σ).symm ⁻¹' s)

A map g between complex coordinate spaces, read in the real coordinates given by TauCeti.complexToRealPi, is semialgebraic on a semialgebraic domain s when its graph over s is cut out by finitely many polynomial equations in the input and output coordinates and their conjugates: for z ∈ s, g z = w exactly when every R k vanishes at (z, w).