Zero-set germs and vanishing ideals in the germ ring 𝒪_n = Conv K n

The definitions of Rückert's Nullstellensatz, stated over any K with [RCLike K]; the theorem itself (Nullstellensatz.lean) is over ℂ. Following [Fre17, Ch. I, §8–§9]: an ideal I ⊆ 𝒪_n is finitely generated (Rückert's basis theorem, isNoetherianRing_conv); the generators converge on a common polydisc around 0, and their common zero set there is the geometric realization V(I) of I, well defined up to shrinking the neighbourhood; the vanishing ideal (Freitag's saturation) of I is the ideal of the series vanishing on V(I) near 0.

• zeroSet S: the common zero set {x | ∀ g ∈ S, g(x) = 0} of a finite family S of convergent series, as a set of points of K^n; only its germ at 0 matters (outside the common polydisc of S the values evalSeries g x are the junk values of a non-summable tsum, and every statement below is an ∀ᶠ x in 𝓝 0 statement, which sees only a neighbourhood of 0 where the finitely many series converge).
• VanishesOn S f: f vanishes on V(S) near 0: ∀ᶠ x in 𝓝 0, x ∈ zeroSet S → f(x) = 0.
• vanishingIdeal I: the series vanishing on V(I) near 0, quantified over every finite system of generators of I (vanishesOn_congr: two systems of generators of the same ideal have the same zero-set germ, so mem_vanishingIdeal_iff reads it off any one of them).

The germs on a manifold vanishing on a set near a point (vanishingStalk) are the same notion on the stalks of an analytic manifold; the two are related where the stalks of an analytic space are identified with convergent series (Hironaka/AnalyticSpace/Nullstellensatz.lean), not here.

Elementary consequences (the trivial inclusions of the proof of [Fre17, Ch. I, 9.1]): I ≤ I.radical ≤ vanishingIdeal I, vanishingIdeal is monotone (V and 𝓘 are both antitone), vanishingIdeal ⊤ = ⊤, and vanishingIdeal ⊥ = ⊥ by the identity theorem (Conv.ext_of_evalSeries_eventuallyEq).

def Analytic.zeroSet {K : Type u_1} [RCLike K] {n : ℕ} (S : Finset ↥(Conv K n)) : Set (Fin n → K)

The common zero set of a finite family S of convergent series, as a set of points of K^n (only its germ at 0 is meaningful): the geometric realization of an ideal of [Fre17, Ch. I, §8].

Equations

• Analytic.zeroSet S = {x : Fin n → K | ∀ g ∈ S, Analytic.evalSeries (↑g) x = 0}

@[simp]

theorem Analytic.mem_zeroSet_iff {K : Type u_1} [RCLike K] {n : ℕ} {S : Finset ↥(Conv K n)} {x : Fin n → K} : x ∈ zeroSet S ↔ ∀ g ∈ S, evalSeries (↑g) x = 0

def Analytic.VanishesOn {K : Type u_1} [RCLike K] {n : ℕ} (S : Finset ↥(Conv K n)) (f : ↥(Conv K n)) : Prop

The series f vanishes on the zero-set germ V(S) near 0.

Equations

• Analytic.VanishesOn S f = ∀ᶠ (x : Fin n → K) in nhds 0, x ∈ Analytic.zeroSet S → Analytic.evalSeries (↑f) x = 0

theorem Analytic.VanishesOn.zero {K : Type u_1} [RCLike K] {n : ℕ} (S : Finset ↥(Conv K n)) : VanishesOn S 0

theorem Analytic.VanishesOn.add {K : Type u_1} [RCLike K] {n : ℕ} {S : Finset ↥(Conv K n)} {f g : ↥(Conv K n)} (hf : VanishesOn S f) (hg : VanishesOn S g) : VanishesOn S (f + g)

theorem Analytic.VanishesOn.mul_left {K : Type u_1} [RCLike K] {n : ℕ} {S : Finset ↥(Conv K n)} (c : ↥(Conv K n)) {f : ↥(Conv K n)} (hf : VanishesOn S f) : VanishesOn S (c * f)

theorem Analytic.VanishesOn.of_mem {K : Type u_1} [RCLike K] {n : ℕ} {S : Finset ↥(Conv K n)} {g : ↥(Conv K n)} (hg : g ∈ S) : VanishesOn S g

theorem Analytic.VanishesOn.of_mem_span {K : Type u_1} [RCLike K] {n : ℕ} {S : Finset ↥(Conv K n)} {g : ↥(Conv K n)} (hg : g ∈ Ideal.span ↑S) : VanishesOn S g

Every element of the ideal generated by S vanishes on V(S) near 0.

theorem Analytic.evalSeries_pow_eventually {K : Type u_1} [RCLike K] {n : ℕ} {f : MvPowerSeries (Fin n) K} (hf : f ∈ Conv K n) (k : ℕ) : evalSeries (f ^ k) =ᶠ[nhds 0] fun (x : Fin n → K) => evalSeries f x ^ k

theorem Analytic.VanishesOn.of_pow {K : Type u_1} [RCLike K] {n : ℕ} {S : Finset ↥(Conv K n)} {f : ↥(Conv K n)} {k : ℕ} (hf : VanishesOn S (f ^ k)) : VanishesOn S f

If a power of f vanishes on V(S) near 0, so does f.

theorem Analytic.eventually_mem_zeroSet_of_span_le {K : Type u_1} [RCLike K] {n : ℕ} {S S' : Finset ↥(Conv K n)} (h : Ideal.span ↑S ≤ Ideal.span ↑S') : ∀ᶠ (x : Fin n → K) in nhds 0, x ∈ zeroSet S' → x ∈ zeroSet S

If span S ≤ span S', then near 0 the zero set of S' lies in the zero set of S (two geometric realizations of the same ideal agree near 0, [Fre17, Ch. I, §8]).

theorem Analytic.vanishesOn_of_span_le {K : Type u_1} [RCLike K] {n : ℕ} {S S' : Finset ↥(Conv K n)} (h : Ideal.span ↑S ≤ Ideal.span ↑S') {f : ↥(Conv K n)} (hf : VanishesOn S f) : VanishesOn S' f

theorem Analytic.vanishesOn_congr {K : Type u_1} [RCLike K] {n : ℕ} {S S' : Finset ↥(Conv K n)} (h : Ideal.span ↑S = Ideal.span ↑S') (f : ↥(Conv K n)) : VanishesOn S f ↔ VanishesOn S' f

The zero-set germ depends only on the ideal generated: vanishing on V(S) near 0 is the same for two finite systems of generators of the same ideal.

def Analytic.vanishingIdeal {K : Type u_1} [RCLike K] {n : ℕ} (I : Ideal ↥(Conv K n)) : Ideal ↥(Conv K n)

The ideal of the series vanishing on the zero-set germ V(I) near 0, read through every finite system of generators of I (they all give the same germ, vanishesOn_congr): the vanishing ideal, Freitag's saturation of I [Fre17, Ch. I, §9].

Equations

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

theorem Analytic.mem_vanishingIdeal_iff {K : Type u_1} [RCLike K] {n : ℕ} {I : Ideal ↥(Conv K n)} {S : Finset ↥(Conv K n)} (hS : Ideal.span ↑S = I) {f : ↥(Conv K n)} : f ∈ vanishingIdeal I ↔ VanishesOn S f

theorem Analytic.exists_finset_span_eq {K : Type u_1} [RCLike K] {n : ℕ} (I : Ideal ↥(Conv K n)) : ∃ (S : Finset ↥(Conv K n)), Ideal.span ↑S = I

Rückert's basis theorem (isNoetherianRing_conv): every ideal of 𝒪_n has a finite system of generators, so every ideal has a zero-set germ.

theorem Analytic.radical_le_vanishingIdeal {K : Type u_1} [RCLike K] {n : ℕ} (I : Ideal ↥(Conv K n)) : I.radical ≤ vanishingIdeal I

√I ⊆ 𝓘(V(I)) (the trivial inclusion of the proof of [Fre17, Ch. I, 9.1]).

theorem Analytic.le_vanishingIdeal {K : Type u_1} [RCLike K] {n : ℕ} (I : Ideal ↥(Conv K n)) : I ≤ vanishingIdeal I

I ⊆ 𝓘(V(I)).

theorem Analytic.vanishingIdeal_mono {K : Type u_1} [RCLike K] {n : ℕ} {I J : Ideal ↥(Conv K n)} (h : I ≤ J) : vanishingIdeal I ≤ vanishingIdeal J

V(J) ⊆ V(I) for I ≤ J, so a series vanishing on V(I) vanishes on V(J): the vanishing ideal is monotone.

theorem Analytic.vanishingIdeal_top {K : Type u_1} [RCLike K] {n : ℕ} : vanishingIdeal ⊤ = ⊤

theorem Analytic.vanishingIdeal_bot {K : Type u_1} [RCLike K] {n : ℕ} : vanishingIdeal ⊥ = ⊥

The identity theorem (Conv.ext_of_evalSeries_eventuallyEq): a series vanishing near 0 is zero, so 𝓘(V(0)) = 0.