The vanishing ideal of a set at a point: basic properties

Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) [Hir64, Main Theorem II'(N) (iii), p. 156] is the reduced closed analytic subspace with a given set of points: its ideal sheaf is, at every point x, the ideal vanishingStalk Z x of the germs of analytic functions vanishing on the set near x (Bierstone–Milman's reduced space, 𝓘_{X_red} = √𝓘_X [BM97, Remark 3.14]; Hironaka's "reduced" means no nilpotent elements [Hir64, p. 111]). This module unfolds the definitions (Germ.vanishesOn_coe, mem_vanishingGermIdeal_iff, mem_vanishingStalk_iff), transports the vanishing of a germ along a surjective embedding (Germ.vanishesOn_compTendsto_of_isEmbedding), and proves the two facts the support of the reduced transform needs: the stalk is the unit ideal exactly off the closure of Z (vanishingStalk_eq_top_of_notMem_closure, vanishingStalk_ne_top_of_mem_closure). Whether these stalks are the stalks of a locally finitely generated ideal sheaf (coherence of the ideal of an analytic set) is a separate question, answered for simple normal crossings divisors in Hironaka/Manifold/Snc/Coherence.lean and left as a guard in the definition of the reduced transform (IdealSheaf.reducedTransform).

theorem Manifold.Germ.vanishesOn_coe {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] (Z : Set M) (x : M) (f : M → 𝕜) : VanishesOn Z x ↑f ↔ ∀ᶠ (y : M) in nhdsWithin x Z, f y = 0

Vanishing of the germ of a function, unfolded.

theorem Manifold.Germ.vanishesOn_compTendsto_of_isEmbedding {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] {Y : Type u_2} [TopologicalSpace Y] {h : M → Y} (hh : Topology.IsEmbedding h) (hs : Function.Surjective h) (Z : Set Y) (x : M) (k : (nhds (h x)).Germ 𝕜) : VanishesOn (h ⁻¹' Z) x (k.compTendsto h ⋯) ↔ VanishesOn Z (h x) k

A germ at h x vanishes on Z iff its composite with the embedding h (onto Y) vanishes on h⁻¹ Z at x.

theorem Manifold.mem_vanishingGermIdeal_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] (Z : Set M) (x : M) (g : (nhds x).Germ 𝕜) : g ∈ vanishingGermIdeal Z x ↔ Germ.VanishesOn Z x g

theorem Manifold.vanishingGermIdeal_eq_top_of_notMem_closure {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] {Z : Set M} {x : M} (hx : x ∉ closure Z) : vanishingGermIdeal Z x = ⊤

Off the closure of Z every germ vanishes on Z near x: the ideal is the unit ideal.

theorem Manifold.vanishingGermIdeal_ne_top_of_mem_closure {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] {Z : Set M} {x : M} (hx : x ∈ closure Z) : vanishingGermIdeal Z x ≠ ⊤

On the closure of Z the constant 1 does not vanish on Z near x: the ideal is proper.

theorem Manifold.mem_vanishingStalk_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ChartedSpace E M] (Z : Set M) (x : M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk x)) : s ∈ vanishingStalk Z x ↔ Germ.VanishesOn Z x ((stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M x) s)

theorem Manifold.vanishingStalk_eq_top_of_notMem_closure {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ChartedSpace E M] {Z : Set M} {x : M} (hx : x ∉ closure Z) : vanishingStalk Z x = ⊤

Off the closure of Z the vanishing ideal is the unit ideal.

theorem Manifold.vanishingStalk_ne_top_of_mem_closure {𝕜 : Type} [NontriviallyNormedField 𝕜] {M : Type u_1} [TopologicalSpace M] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ChartedSpace E M] {Z : Set M} {x : M} (hx : x ∈ closure Z) : vanishingStalk Z x ≠ ⊤

On the closure of Z the vanishing ideal is proper (the constant 1 does not vanish).