Rückert's local analytic Nullstellensatz

The prepared-prime argument supplies the prime zero-set theorem in every dimension. This module exposes its unconditional ideal-theoretic and representative-level consequences.

theorem LocalComplexGeometry.analyticNullstellensatz_ideal {n : ℕ} (I : Ideal ↥(HolomorphicGerm n)) : vanishingIdeal (idealZeroSetGerm I) = I.radical

The ideal of germs vanishing on the local zero set of an arbitrary ideal is its radical.

theorem LocalComplexGeometry.vanishingIdeal_idealZeroSetGerm_eq_radical_unconditional {n : ℕ} (I : Ideal ↥(HolomorphicGerm n)) : vanishingIdeal (idealZeroSetGerm I) = I.radical

A descriptive alias for the unconditional ideal form of the local analytic Nullstellensatz.

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

Rückert's local analytic Nullstellensatz for a finite family of analytic representatives. A germ vanishing on their local common zero set has a positive power in the ideal they generate.

theorem LocalComplexGeometry.localAnalyticNullstellensatz_empty {n : ℕ} {g : ComplexEuclidean n → ℂ} (hg : AnalyticAt ℂ g 0) (hzero : g =ᶠ[nhds 0] fun (x : ComplexEuclidean n) => 0) : ∃ (N : ℕ), 0 < N ∧ (fun (x : ComplexEuclidean n) => g x ^ N) =ᶠ[nhds 0] fun (x : ComplexEuclidean n) => 0

Empty-family form: an analytic representative which is locally zero has a positive power which is locally zero.