Reduction of the analytic Nullstellensatz to prime ideals

This module contains no geometric assertion about prime ideals. Instead it isolates that assertion as PrimeZeroSetProperty and proves that it suffices for the radical theorem, the finite-family representative-level theorem, and the arbitrary-ideal zero-set equality.

def LocalComplexGeometry.PrimeZeroSetProperty (n : ℕ) : Prop

The prime-ideal zero-set statement in complex dimension n: every prime ideal is exactly the ideal of holomorphic germs vanishing on the local zero-set germ of any finite generating set selected for that prime.

Equations

• One or more equations did not get rendered due to their size.

theorem LocalComplexGeometry.vanishingIdeal_isRadical {n : ℕ} (Z : LocalSetGerm n) : (vanishingIdeal Z).IsRadical

Vanishing on a fixed local set germ is a radical condition.

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

Prime zero-set information implies the arbitrary-ideal radical equality.

The proof intersects the minimal primes above I. It also applies to I = ⊤: then the set of minimal primes is empty and its infimum is ⊤.

theorem LocalComplexGeometry.vanishingIdeal_idealZeroSetGerm_top_of_primeZeroSetProperty {n : ℕ} (hprime : PrimeZeroSetProperty n) : vanishingIdeal (idealZeroSetGerm ⊤) = ⊤

Explicit I = ⊤ specialization of the radical reduction.

theorem LocalComplexGeometry.finiteCommonZeroSet_image_univ_eq_indexedCommonZeroSet {n s : ℕ} (f : Fin s → ↥(HolomorphicGerm n)) : finiteCommonZeroSet (Finset.image f Finset.univ) = indexedCommonZeroSet f

The zero set of a finite image is the indexed common zero-set germ.

theorem LocalComplexGeometry.span_image_univ_eq_span_range {n s : ℕ} (f : Fin s → ↥(HolomorphicGerm n)) : Ideal.span ↑(Finset.image f Finset.univ) = Ideal.span (Set.range f)

The ideal spanned by a finite image is the ideal spanned by its range.

theorem LocalComplexGeometry.localAnalyticNullstellensatz_of_primeZeroSetProperty {n s : ℕ} (hprime : PrimeZeroSetProperty n) {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

The exact comparator-facing finite-family Nullstellensatz follows from the prime zero-set property. The exponent is made positive by replacing an arbitrary radical witness k by k + 1; this also handles the case where the generated ideal is ⊤.

theorem LocalComplexGeometry.localAnalyticNullstellensatz_empty_of_primeZeroSetProperty {n : ℕ} (hprime : PrimeZeroSetProperty 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

The empty-family specialization. Its common-zero hypothesis says exactly that g is the zero germ, and the general reduction still returns a positive exponent.