Holomorphic inverse function theorem on surfaces

Unit: surfaces-and-charts (docs/design/surfaces-and-charts.md §3.5; Forster 2.1/2.5 local part).

• exists_openPartialHomeomorph_of_deriv_ne_zero: if f : X → Y is holomorphic at x with nonvanishing chart-derivative, there is an OpenPartialHomeomorph X Y around x agreeing with f that is holomorphic with holomorphic inverse;
• mfderiv_ne_zero_iff_deriv_ne_zero: the chart-free (invariant) form of the hypothesis;
• exists_openPartialHomeomorph_of_mfderiv_ne_zero: the IFT keyed on mfderiv (invariant interface for mapping-degree);
• map_nhds_eq_of_deriv_ne_zero: local-homeomorphism consequence, f maps neighborhoods onto neighborhoods.

The planar input is mathlib's analytic inverse function theorem (AnalyticAt.analyticAt_localInverse, HasStrictFDerivAt.toOpenPartialHomeomorph).

theorem RS.exists_openPartialHomeomorph_of_deriv_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) (hf' : deriv (writtenInExtChartAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) x f) (↑(extChartAt (modelWithCornersSelf ℂ ℂ) x) x) ≠ 0) : ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e) e.source ∧ ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑e) e.source ∧ ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑e.symm) e.target

Holomorphic inverse function theorem on surfaces. If f is holomorphic at x with nonvanishing chart-derivative, there is a partial homeomorphism around x agreeing with f that is holomorphic with holomorphic inverse.

theorem RS.mfderiv_ne_zero_iff_deriv_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} (hf : MDiffAt f x) : mfderiv% f x ≠ 0 ↔ deriv (writtenInExtChartAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) x f) (↑(extChartAt (modelWithCornersSelf ℂ ℂ) x) x) ≠ 0

The chart-free (invariant) form of the nonvanishing-derivative hypothesis.

theorem RS.exists_openPartialHomeomorph_of_mfderiv_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) (hf' : mfderiv% f x ≠ 0) : ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e) e.source ∧ ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑e) e.source ∧ ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑e.symm) e.target

IFT keyed on mfderiv (invariant interface for mapping-degree).

theorem RS.map_nhds_eq_of_deriv_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) (hf' : deriv (writtenInExtChartAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) x f) (↑(extChartAt (modelWithCornersSelf ℂ ℂ) x) x) ≠ 0) : Filter.map f (nhds x) = nhds (f x)

Local-homeomorphism consequence: f maps neighborhoods onto neighborhoods.