Regular holomorphic level sets

A surjective derivative at one point gives a local analytic parametrization of the corresponding fiber. The parameter space has the expected complex dimension n - m. Besides the analytic parameter map, the interface exposes an analytic ambient fiber-coordinate map and eventual two-sided inverse laws, so the conclusion is stronger than a dimension count.

structure LocalComplexGeometry.IsLocalLevelSetParametrization {n m : ℕ} (F : ComplexEuclidean n → ComplexEuclidean m) (a : ComplexEuclidean n) (parameter : ComplexEuclidean (n - m) → ComplexEuclidean n) (fiberCoordinate : ComplexEuclidean n → ComplexEuclidean (n - m)) : Prop

An explicit local analytic parametrization of the fiber F⁻¹(F a) by ℂ^(n-m).

The parameter and fiber-coordinate maps are analytic at their marked points. They are locally inverse on the parameter space and on the level set, and the parameter map lands in the level set on a neighborhood of the origin.

• parameter_zero : parameter 0 = a
• fiberCoordinate_base : fiberCoordinate a = 0
• analyticAt_parameter : AnalyticAt ℂ parameter 0
• analyticAt_fiberCoordinate : AnalyticAt ℂ fiberCoordinate a
• left_inv : (fun (u : ComplexEuclidean (n - m)) => fiberCoordinate (parameter u)) =ᶠ[nhds 0] fun (u : ComplexEuclidean (n - m)) => u
• parameter_mem_fiber : (fun (u : ComplexEuclidean (n - m)) => F (parameter u)) =ᶠ[nhds 0] fun (x : ComplexEuclidean (n - m)) => F a
• right_inv_on_fiber : ∀ᶠ (x : ComplexEuclidean n) in nhds a, F x = F a → parameter (fiberCoordinate x) = x

theorem LocalComplexGeometry.IsLocalLevelSetParametrization.eventually_mem_fiber_iff {n m : ℕ} {F : ComplexEuclidean n → ComplexEuclidean m} {a : ComplexEuclidean n} {parameter : ComplexEuclidean (n - m) → ComplexEuclidean n} {fiberCoordinate : ComplexEuclidean n → ComplexEuclidean (n - m)} (h : IsLocalLevelSetParametrization F a parameter fiberCoordinate) : ∀ᶠ (x : ComplexEuclidean n) in nhds a, F x = F a ↔ parameter (fiberCoordinate x) = x

Near the base point, membership in the regular level set is exactly recovery by the local parameter/fiber-coordinate pair.

theorem LocalComplexGeometry.IsLocalLevelSetParametrization.exists_mem_nhds_parameter_injOn {n m : ℕ} {F : ComplexEuclidean n → ComplexEuclidean m} {a : ComplexEuclidean n} {parameter : ComplexEuclidean (n - m) → ComplexEuclidean n} {fiberCoordinate : ComplexEuclidean n → ComplexEuclidean (n - m)} (h : IsLocalLevelSetParametrization F a parameter fiberCoordinate) : ∃ s ∈ nhds 0, Set.InjOn parameter s

The parameter map is injective on some neighborhood of the origin.

theorem LocalComplexGeometry.holomorphic_regularLevelSet_parametrization {n m : ℕ} {F : ComplexEuclidean n → ComplexEuclidean m} {a : ComplexEuclidean n} (hF : AnalyticAt ℂ F a) (hsurj : Function.Surjective ⇑(fderiv ℂ F a)) : ∃ (parameter : ComplexEuclidean (n - m) → ComplexEuclidean n) (fiberCoordinate : ComplexEuclidean n → ComplexEuclidean (n - m)), IsLocalLevelSetParametrization F a parameter fiberCoordinate

Holomorphic regular level-set theorem. If the derivative of a holomorphic map is surjective at a, then the local fiber through a is analytically parametrized by a neighborhood of the origin in ℂ^(n-m), with an analytic local inverse defined on the ambient source.

Only surjectivity at the marked point is assumed; no separate neighborhood constant-rank hypothesis is needed.