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.
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)
:
Ruckert's local analytic Nullstellensatz.