Zero-set germs under a linear change, graphs as zero sets, and consequences of the Nullstellensatz

Tools for the density of the simple points of a reduced complex space ([Fre17, Ch. II, 5.13], through the local parametrization theorem of ParametrizationGraph.lean): the zero-set germ of σ⁻¹(S), σ = substEquiv L, is L (V(S)) (eventually_mem_zeroSet_image_symm_iff, with span_image_symm : span σ⁻¹(S) = comap σ (span S), the generating system of an ideal in the coordinates of σ); the graph of an analytic section φ of the base projection through a point x is, near x, the common zero set of the series X_j − T_j(X ∘ e) over the fibre coordinates, T_j the Taylor series of u ↦ φ (x ∘ e + u) j − x j (exists_conv_eventuallyEq_shift, eventually_graph_eq_zero_iff); and two consequences of Rückert's Nullstellensatz (Nullstellensatz.lean): radical ideals with the same zero-set germ are equal (eq_of_isRadical_of_zeroSet_eventuallyEq), and a prime's zero set has points arbitrarily near 0 off any g ∉ P (frequently_mem_zeroSet_and_ne_zero; the zero set of g is thin at 0, [Fre17, Ch. I, 9.2–9.3]). The zero sets and vanishing ideals are those of ZeroSet.lean, the substitutions those of Subst.lean.

theorem Analytic.substEquiv_symm_apply {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) (f : ↥(Conv K n)) : (substEquiv L).symm f = substConv (↑L.symm) f

σ⁻¹ f is the substitution of L⁻¹.

theorem Analytic.eventually_mem_zeroSet_image_symm_iff {K : Type u_1} [RCLike K] {n : ℕ} [DecidableEq ↥(Conv K n)] (L : (Fin n → K) ≃L[K] Fin n → K) (S : Finset ↥(Conv K n)) : ∀ᶠ (x : Fin n → K) in nhds 0, x ∈ zeroSet (Finset.image (⇑(substEquiv L).symm) S) ↔ L.symm x ∈ zeroSet S

The zero set of σ⁻¹(S) near 0 is L (V(S)).

theorem Analytic.span_image_symm {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) (S : Finset ↥(Conv K n)) [DecidableEq ↥(Conv K n)] : Ideal.span ↑(Finset.image (⇑(substEquiv L).symm) S) = Ideal.comap (substEquiv L) (Ideal.span ↑S)

span σ⁻¹(S) = comap σ (span S): a generating system of the ideal in the coordinates of σ.

theorem Analytic.eq_of_isRadical_of_zeroSet_eventuallyEq {n : ℕ} {I₁ I₂ : Ideal ↥(Conv ℂ n)} (h₁ : I₁.IsRadical) (h₂ : I₂.IsRadical) {S₁ S₂ : Finset ↥(Conv ℂ n)} (hS₁ : Ideal.span ↑S₁ = I₁) (hS₂ : Ideal.span ↑S₂ = I₂) (h : ∀ᶠ (x : Fin n → ℂ) in nhds 0, x ∈ zeroSet S₁ ↔ x ∈ zeroSet S₂) : I₁ = I₂

Rückert's Nullstellensatz for radical ideals with the same zero-set germ: they are equal.

theorem Analytic.frequently_mem_zeroSet_and_ne_zero {n : ℕ} {P : Ideal ↥(Conv ℂ n)} [hP : P.IsPrime] {S : Finset ↥(Conv ℂ n)} (hS : Ideal.span ↑S = P) {g : ↥(Conv ℂ n)} (hg : g ∉ P) : ∃ᶠ (x : Fin n → ℂ) in nhds 0, x ∈ zeroSet S ∧ evalSeries (↑g) x ≠ 0

Rückert's contrapositive: off a series g ∉ P, the zero set of the prime P has points arbitrarily near 0.

theorem Analytic.exists_conv_eventuallyEq_shift {d : ℕ} {g : (Fin d → ℂ) → ℂ} {u₀ : Fin d → ℂ} (hg : AnalyticAt ℂ g u₀) : ∃ (T : ↥(Conv ℂ d)), ∀ᶠ (u : Fin d → ℂ) in nhds 0, g (u₀ + u) = evalSeries (↑T) u

The Taylor series at 0 of u ↦ g (u₀ + u) for g analytic at u₀.

theorem Analytic.evalSeries_conv_sub_eventually {n : ℕ} (f g : ↥(Conv ℂ n)) : evalSeries ↑(f - g) =ᶠ[nhds 0] fun (x : Fin n → ℂ) => evalSeries (↑f) x - evalSeries (↑g) x

Conv-level evaluation of a difference near 0.

theorem Analytic.eventually_graph_eq_zero_iff {n d : ℕ} (e : Fin d ↪ Fin n) (φ : (Fin d → ℂ) → Fin n → ℂ) (x : Fin n → ℂ) (hφe : ∀ (u : Fin d → ℂ), φ u ∘ ⇑e = u) (T : Fin n → ↥(Conv ℂ d)) (hT : ∀ j ∉ Set.range ⇑e, ∀ᶠ (u : Fin d → ℂ) in nhds 0, φ (x ∘ ⇑e + u) j - x j = evalSeries (↑(T j)) u) : ∀ᶠ (y' : Fin n → ℂ) in nhds 0, (∀ j ∉ Set.range ⇑e, evalSeries (↑(convX ℂ j - (convEmbed ℂ e) (T j))) y' = 0) ↔ x + y' = φ ((x + y') ∘ ⇑e)

The graph of a section φ of the base projection through x, as the common zero set near 0 of the series X_j − T_j(X ∘ e) over the fibre coordinates, T_j the Taylor series of u ↦ φ (x ∘ e + u) j − x j.