Palomar-facing theorem surface

The theorem statements in this module use only Mathlib objects and the elementary definition of a holomorphic germ. The implementation-specific coordinate, quotient-basis, and local-biholomorphism structures remain in the proof development and are eliminated from the public statement surface.

theorem LocalComplexGeometry.holomorphicGerm_isNoetherian (n : ℕ) : have O := fun (k : ℕ) => { carrier := {phi : (nhds 0).Germ ℂ | ∃ (f : (Fin k → ℂ) → ℂ), AnalyticAt ℂ f 0 ∧ ↑f = phi}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }; IsNoetherianRing ↥(O n)

Ruckert's basis theorem. The analytic function-germ ring is Noetherian in every finite complex dimension. The ring is defined locally in the statement so the compared type contains only Mathlib constants.

theorem LocalComplexGeometry.hypersurface_finiteProjection : let E := fun (k : ℕ) => Fin k → ℂ; let G := fun (k : ℕ) => (nhds 0).Germ ℂ; let O := fun (k : ℕ) => { carrier := {phi : G k | ∃ (f : E k → ℂ), AnalyticAt ℂ f 0 ∧ ↑f = phi}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }; ∀ {n : ℕ} {f : ↥(O (n + 1))}, f ≠ 0 → Filter.Germ.value ↑f = 0 → ∃ (L : E (n + 1) ≃L[ℂ] E (n + 1)) (d : ℕ) (H : E (n + 1) → ℂ) (F : E (n + 1) → ℂ) (g : ↥(O (n + 1))), 0 < d ∧ AnalyticAt ℂ H 0 ∧ ↑H = ↑f ∧ AnalyticAt ℂ F 0 ∧ ↑F = ↑(H ∘ ⇑L) ∧ ↑g = ↑F ∧ have I := Ideal.span {g}; have q := Ideal.Quotient.mk I; (∃ (ι : ↥(O n) →+* ↥(O (n + 1))) (w : ↥(O (n + 1))), (∀ (a : ↥(O n)) (A : E n → ℂ), AnalyticAt ℂ A 0 → ↑A = ↑a → (↑fun (x : E (n + 1)) => A fun (i : Fin n) => x i.castSucc) = ↑(ι a)) ∧ (↑fun (x : E (n + 1)) => x (Fin.last n)) = ↑w ∧ ∀ (y : ↥(O (n + 1)) ⧸ I), ∃! c : Fin d → ↥(O n), y = ∑ i : Fin d, q (ι (c i) * w ^ ↑i)) ∧ ∃ (a : Fin d → E n → ℂ) (u : E (n + 1) → ℂ) (U : Set (E n)) (R : ℝ), IsOpen U ∧ 0 ∈ U ∧ IsPreconnected U ∧ 0 < R ∧ AnalyticOnNhd ℂ F {x : E (n + 1) | (fun (i : Fin n) => x i.castSucc) ∈ U ∧ ‖x (Fin.last n)‖ < R} ∧ (∀ (i : Fin d), AnalyticOnNhd ℂ (a i) U) ∧ AnalyticOnNhd ℂ u {x : E (n + 1) | (fun (i : Fin n) => x i.castSucc) ∈ U ∧ ‖x (Fin.last n)‖ < R} ∧ (∀ (i : Fin d), a i 0 = 0) ∧ (∀ (x : E (n + 1)), (fun (i : Fin n) => x i.castSucc) ∈ U → ‖x (Fin.last n)‖ < R → F x = u x * (x (Fin.last n) ^ d + ∑ i : Fin d, (a i fun (j : Fin n) => x j.castSucc) * x (Fin.last n) ^ ↑i)) ∧ (∀ (x : E (n + 1)), (fun (i : Fin n) => x i.castSucc) ∈ U → ‖x (Fin.last n)‖ < R → u x ≠ 0) ∧ (∀ z ∈ U, ∀ (w : ℂ), ‖w‖ = R → w ^ d + ∑ i : Fin d, a i z * w ^ ↑i ≠ 0) ∧ (∀ z ∈ U, ∀ (w : ℂ), ‖w‖ = R → (F fun (i : Fin (n + 1)) => Fin.lastCases w z i) ≠ 0) ∧ (∀ z ∈ U, {w : ℂ | ‖w‖ < R ∧ (F fun (i : Fin (n + 1)) => Fin.lastCases w z i) = 0}.Finite) ∧ (∀ z ∈ U, {w : ℂ | ‖w‖ < R ∧ (F fun (i : Fin (n + 1)) => Fin.lastCases w z i) = 0}.ncard ≤ d) ∧ (Function.Surjective fun (x : { x : E (n + 1) // (fun (i : Fin n) => x i.castSucc) ∈ U ∧ ‖x (Fin.last n)‖ < R ∧ F x = 0 }) => ⟨fun (i : Fin n) => ↑x i.castSucc, ⋯⟩) ∧ IsProperMap fun (x : { x : E (n + 1) // (fun (i : Fin n) => x i.castSucc) ∈ U ∧ ‖x (Fin.last n)‖ < R ∧ F x = 0 }) => ⟨fun (i : Fin n) => ↑x i.castSucc, ⋯⟩

Finite projection for a nontrivial analytic hypersurface germ.

This compared wrapper defines the analytic-germ rings locally, so its type is Mathlib-only. It is definitionally the expanded implementation theorem above.

theorem LocalComplexGeometry.holomorphic_constantRank_normalForm {n m r : ℕ} {F : (Fin n → ℂ) → Fin m → ℂ} {a : Fin n → ℂ} (hF : AnalyticAt ℂ F a) (hrn : r ≤ n) (hrm : r ≤ m) (hconst : ∀ᶠ (x : Fin n → ℂ) in nhds a, Module.finrank ℂ ↥(↑(fderiv ℂ F x)).range = r) : ∃ (sourceCoord : (Fin n → ℂ) → Fin n → ℂ) (sourceInv : (Fin n → ℂ) → Fin n → ℂ) (targetCoord : (Fin m → ℂ) → Fin m → ℂ) (targetInv : (Fin m → ℂ) → Fin m → ℂ), sourceCoord a = 0 ∧ sourceInv 0 = a ∧ targetCoord (F a) = 0 ∧ targetInv 0 = F a ∧ AnalyticAt ℂ sourceCoord a ∧ AnalyticAt ℂ sourceInv 0 ∧ AnalyticAt ℂ targetCoord (F a) ∧ AnalyticAt ℂ targetInv 0 ∧ ((fun (x : Fin n → ℂ) => sourceInv (sourceCoord x)) =ᶠ[nhds a] fun (x : Fin n → ℂ) => x) ∧ ((fun (x : Fin n → ℂ) => sourceCoord (sourceInv x)) =ᶠ[nhds 0] fun (x : Fin n → ℂ) => x) ∧ ((fun (y : Fin m → ℂ) => targetInv (targetCoord y)) =ᶠ[nhds (F a)] fun (y : Fin m → ℂ) => y) ∧ ((fun (y : Fin m → ℂ) => targetCoord (targetInv y)) =ᶠ[nhds 0] fun (y : Fin m → ℂ) => y) ∧ (fun (x : Fin n → ℂ) => targetCoord (F (sourceInv x))) =ᶠ[nhds 0] fun (x : Fin n → ℂ) (j : Fin m) => if h : ↑j < r then x ⟨↑j, ⋯⟩ else 0

The holomorphic constant-rank normal form in direct coordinates.

theorem LocalComplexGeometry.localAnalyticNullstellensatz {n s : ℕ} {f : Fin s → (Fin n → ℂ) → ℂ} {g : (Fin n → ℂ) → ℂ} (hf : ∀ (i : Fin s), AnalyticAt ℂ (f i) 0) (hg : AnalyticAt ℂ g 0) (hzero : ∀ᶠ (x : Fin n → ℂ) in nhds 0, (∀ (i : Fin s), f i x = 0) → g x = 0) : ∃ (N : ℕ), 0 < N ∧ ∃ (h : Fin s → (Fin n → ℂ) → ℂ), (∀ (i : Fin s), AnalyticAt ℂ (h i) 0) ∧ (fun (x : Fin n → ℂ) => g x ^ N) =ᶠ[nhds 0] fun (x : Fin n → ℂ) => ∑ i : Fin s, h i x * f i x

Ruckert's local analytic Nullstellensatz.