5.5. Surface.ManifoldIFT🔗

Jacobians.Surface.ManifoldIFT — source

exists_holo_localInverse

Manifold inverse function theorem (local holomorphic section). For f : X → Y real-analytic between complex 1-manifolds, with non-vanishing chart-pullback derivative at x, there is a C^ω local section g of f defined on an open neighborhood V of f x, with g (f x) = x and f (g y) = y for y ∈ V.

theorem exists_holo_localInverse
    {X Y : Type*}
    [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (x : X)
    (hderiv : deriv ((chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm) ((chartAt ℂ x) x) ≠ 0) :
    ∃ (g : Y → X) (V : Set Y), IsOpen V ∧ f x ∈ V ∧ g (f x) = x ∧
      (∀ y ∈ V, f (g y) = y) ∧ ContMDiffOn 𝓘(ℂ) 𝓘(ℂ) ω g V