Complexification of analytic charts

A real analytic chart and its analytic inverse extend together to a holomorphic chart near each real point of its source. The complex chart and its inverse agree with the original maps near the corresponding real points and commute with conjugation. This allows changes to analytic coordinates before applying holomorphic polynomial root theorems.

The identity theorem on real points transports the two inverse identities to complex neighborhoods. Restricting those neighborhoods then gives an open partial homeomorphism; no choice of a derivative or complex linear extension of a derivative is needed.

References

• S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Chapter 2.

theorem OpenPartialHomeomorph.exists_complexification {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : OpenPartialHomeomorph (ι → ℝ) (κ → ℝ)) {a : ι → ℝ} (ha : a ∈ e.source) (he : AnalyticAt ℝ (↑e) a) (he' : AnalyticAt ℝ (↑e.symm) (↑e a)) : ∃ (E : OpenPartialHomeomorph (ι → ℂ) (κ → ℂ)), (fun (i : ι) => ↑(a i)) ∈ E.source ∧ AnalyticOnNhd ℂ (↑E) E.source ∧ AnalyticOnNhd ℂ (↑E.symm) E.target ∧ (∀ᶠ (x : ι → ℝ) in nhds a, (↑E fun (i : ι) => ↑(x i)) = fun (i : κ) => ↑(↑e x i)) ∧ (∀ᶠ (y : κ → ℝ) in nhds (↑e a), (↑E.symm fun (i : κ) => ↑(y i)) = fun (i : ι) => ↑(↑e.symm y i)) ∧ (∀ (z : ι → ℂ), ↑E (star z) = star (↑E z)) ∧ ∀ (z : κ → ℂ), ↑E.symm (star z) = star (↑E.symm z)

A real chart analytic at a source point, with inverse analytic at its image, extends to a complex chart analytic on its source with analytic inverse on its target. Both maps agree with the original chart near the real points and commute with conjugation at every complex point.