The two vanishing ideals of a set at a point of a manifold agree

The ideal vanishingStalk Z x ⊆ 𝒪_{M,x} is the ideal of the germs vanishing on Z near x, for a manifold M; Hironaka/AnalyticSpace/VanishingIdeal.lean defines, for a locally ringed space X, the ideal vanishingStalkIdeal X C y of the germs at y of sections whose value vanishes at every point of C near y — the ideal Rückert's Nullstellensatz computes as the radical of a stalk ideal (radical_stalkIdeal_eq_vanishingStalkIdeal, at the analytic space of a complex manifold). In the stalk 𝒪_{M,x} = 𝒪_{Sp(M),x} (the analytic space Sp(M) of M carries the structure sheaf of M, Hironaka/AnalyticSpace/Manifold/Defs.lean) the two ideals coincide, since a germ vanishes at a point iff it lies in the maximal ideal there (vanishingStalk_eq_vanishingStalkIdeal). This is the bridge by which the Nullstellensatz is read on the manifold-side vanishing ideals. Not in the sources; bookkeeping between the two definitions.

theorem Manifold.germ_mem_maximalIdeal_iff_extendSection {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {V : TopologicalSpace.Opens M} {y : M} (hy : y ∈ V) (g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V y hy)) g ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk y) ↔ extendSection 𝕜 E g y = 0

The germ of a section lies in the maximal ideal at y iff the section's value at y vanishes.

@[reducible, inline]

noncomputable abbrev Manifold.toSpaceLRS {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] : AlgebraicGeometry.LocallyRingedSpace

The analytic space Sp(M) of the manifold M, as a locally ringed space: its structure sheaf is structureSheaf 𝕜 E M. The form in which Rückert's theorem (radical_stalkIdeal_eq_vanishingStalkIdeal) is stated.

Equations

• Manifold.toSpaceLRS ψ = (AnalyticSpace.toSpace ψ { carrier := M, top := inst✝⁴, charted := inst✝³, manifold := inst✝², t2 := inst✝¹, secondCountable := inst✝ }).toLocallyRingedSpace

theorem Manifold.mem_vanishingStalkIdeal_toSpaceLRS_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] (Z : Set M) (x : M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk x)) : s ∈ AnalyticSpace.vanishingStalkIdeal (toSpaceLRS ψ) Z x ↔ ∃ (V : TopologicalSpace.Opens M) (hy : x ∈ V) (g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V x hy)) g = s ∧ ∀ (y' : M) (hy' : y' ∈ V), y' ∈ Z → (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V y' hy')) g ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk y')

Membership in the space-side vanishing ideal of Sp(M), read on the structure sheaf of M.

theorem Manifold.vanishingStalk_eq_vanishingStalkIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] (Z : Set M) (x : M) : vanishingStalk Z x = AnalyticSpace.vanishingStalkIdeal (toSpaceLRS ψ) Z x

The manifold-side vanishing ideal of Z at x is the space-side vanishing ideal of Z at x in Sp(M).