Holomorphic constant-rank theorem

This file proves the local analytic normal form for a holomorphic map of constant complex rank. The proof uses the analytic inverse-function theorem, finite-dimensional complements, and the mean-value theorem on the kernel factor.

theorem LocalComplexGeometry.eventually_snd_eq_slice_of_rank {U : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup U] [NormedSpace ℂ U] [FiniteDimensional ℂ U] [CompleteSpace U] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {P : U × V → U × W} (hP : AnalyticAt ℂ P 0) (hfst : (fun (z : U × V) => (P z).1) =ᶠ[nhds 0] fun (z : U × V) => z.1) (hrank : ∀ᶠ (z : U × V) in nhds 0, complexLinearRank (fderiv ℂ P z) = Module.finrank ℂ U) : (fun (z : U × V) => (P z).2) =ᶠ[nhds 0] fun (z : U × V) => (P (z.1, 0)).2

Once the first component of an analytic map is the first projection and the derivative has the minimal possible rank, the second component is locally independent of the second input variable.

theorem LocalComplexGeometry.holomorphic_constant_rank {n m r : ℕ} {F : ComplexEuclidean n → ComplexEuclidean m} {a : ComplexEuclidean n} (hF : AnalyticAt ℂ F a) (hrn : r ≤ n) (hrm : r ≤ m) (hconst : ∀ᶠ (x : ComplexEuclidean n) in nhds a, complexRank (fderiv ℂ F x) = r) : ∃ (phi : LocalBiholomorphAt (ComplexEuclidean n) (ComplexEuclidean n) a 0) (psi : LocalBiholomorphAt (ComplexEuclidean m) (ComplexEuclidean m) (F a) 0), (fun (x : ComplexEuclidean n) => psi.toFun (F (phi.invFun x))) =ᶠ[nhds 0] standardRankMap n m r

Holomorphic constant-rank theorem. A holomorphic map whose complex rank is locally constant is locally equivalent, through biholomorphic source and target coordinates centered at the origin, to the standard coordinate map of that rank.

theorem LocalComplexGeometry.holomorphic_constantRank_normalForm_core {n m r : ℕ} {F : ComplexEuclidean n → ComplexEuclidean m} {a : ComplexEuclidean n} (hF : AnalyticAt ℂ F a) (hrn : r ≤ n) (hrm : r ≤ m) (hconst : ∀ᶠ (x : ComplexEuclidean n) in nhds a, complexRank (fderiv ℂ F x) = r) : ∃ (phi : LocalBiholomorphAt (ComplexEuclidean n) (ComplexEuclidean n) a 0) (psi : LocalBiholomorphAt (ComplexEuclidean m) (ComplexEuclidean m) (F a) 0), (fun (x : ComplexEuclidean n) => psi.toFun (F (phi.invFun x))) =ᶠ[nhds 0] standardRankMap n m r

Audited public spelling of holomorphic_constant_rank.

theorem LocalComplexGeometry.holomorphic_submersion_normalForm {n m : ℕ} {F : ComplexEuclidean n → ComplexEuclidean m} {a : ComplexEuclidean n} (hF : AnalyticAt ℂ F a) (hsurj : ∀ᶠ (x : ComplexEuclidean n) in nhds a, Function.Surjective ⇑(fderiv ℂ F x)) : ∃ (phi : LocalBiholomorphAt (ComplexEuclidean n) (ComplexEuclidean n) a 0) (psi : LocalBiholomorphAt (ComplexEuclidean m) (ComplexEuclidean m) (F a) 0), (fun (x : ComplexEuclidean n) => psi.toFun (F (phi.invFun x))) =ᶠ[nhds 0] standardRankMap n m m

A holomorphic map with locally surjective derivative has the standard submersion normal form. The necessary inequality m ≤ n is a consequence, not an extra hypothesis.

theorem LocalComplexGeometry.holomorphic_immersion_normalForm {n m : ℕ} {F : ComplexEuclidean n → ComplexEuclidean m} {a : ComplexEuclidean n} (hF : AnalyticAt ℂ F a) (hinj : ∀ᶠ (x : ComplexEuclidean n) in nhds a, Function.Injective ⇑(fderiv ℂ F x)) : ∃ (phi : LocalBiholomorphAt (ComplexEuclidean n) (ComplexEuclidean n) a 0) (psi : LocalBiholomorphAt (ComplexEuclidean m) (ComplexEuclidean m) (F a) 0), (fun (x : ComplexEuclidean n) => psi.toFun (F (phi.invFun x))) =ᶠ[nhds 0] standardRankMap n m n

A holomorphic map with locally injective derivative has the standard immersion normal form. The necessary inequality n ≤ m is a consequence, not an extra hypothesis.