Rückert's Nullstellensatz for the stalks of an analytic ℂ-space

The ideal of the germs vanishing on the support of an ideal sheaf J of finite type is the radical of J, stalk by stalk: 𝓘_{S(J)}(y) = √(J_y) (vanishingStalkIdeal_cosupport_eq_radical) — the Nullstellensatz for analytic sets [GR84, Ch. 4, §1]. It is Rückert's Nullstellensatz for 𝒪_n = Conv ℂ n (vanishingIdeal_eq_radical, Hironaka/Analytic/Rueckert/Nullstellensatz.lean), carried to the stalks of an analytic space in three steps:

• vanishingStalkIdeal_eq_radical_span_affine: at a point q ∈ ℂⁿ, for a set D which near q is the common zero set of finitely many analytic functions h_i, the germs vanishing on D are the radical of (h_1, …, h_k)_q — the Taylor isomorphism taylorAffine q : 𝒜_{ℂⁿ,q} ≃ 𝒪_n (Hironaka/AnalyticSpace/Dimension.lean) turns the zero set into the zero-set germ V(S) of the Taylor series S and the vanishing condition into VanishesOn S, and Rückert's theorem finishes.
• vanishingStalkIdeal_cosupport_eq_radical_analyticSpaceOfOpen: the open subspace (G, 𝒜_G), along the open immersion into (ℂⁿ, 𝒜) (stalk isomorphisms); the support of J is the common zero set of local generators (a local ring: a span is proper iff no generator is a unit, and a germ is a unit iff its value is nonzero).
• vanishingStalkIdeal_cosupport_eq_radical_quotient: a quotient (S(𝒥), 𝒪_Y/𝒥), along its closed immersion (surjective stalk maps), given the statement on Y for the lifted ideal sheaf (liftIdeal, Hironaka/AnalyticSpace/QuotientLift.lean).

The general statement then follows through a chart X|U ≅ (S(𝓘), 𝒜_G/𝓘) (exists_kIso_localModel) with the transport of ideal sheaves restrictIdeal (Hironaka/AnalyticSpace/QuotientMap.lean) and comap, points being parametrized from the model side. isUnit_map_iff_of_bijective and germ_mem_maximalIdeal_affine_iff are the two small tools. Used by Hironaka/Manifold/BlowUp/Transform/StrictSubspaceClosure.lean.

theorem AnalyticSpace.germ_mem_maximalIdeal_affine_iff {n : ℕ} {K : Type} [RCLike K] (U : TopologicalSpace.Opens (Kn K n)) (x : ↥U) (g : AnalyticFun K n U) : (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ U ↑x ⋯)) g ∈ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk ↑x) ↔ g.eval x = 0

A germ of 𝒜_{Kⁿ} lies in the maximal ideal iff the function vanishes at the point.

theorem AnalyticSpace.vanishingStalkIdeal_eq_radical_span_affine {n : ℕ} (q : Kn ℂ n) {U : TopologicalSpace.Opens (Kn ℂ n)} (hq : q ∈ U) {k : ℕ} (h : Fin k → AnalyticFun ℂ n U) {D : Set (Kn ℂ n)} (hD : ∀ (b : Kn ℂ n) (hb : b ∈ U), b ∈ D ↔ ∀ (i : Fin k), (h i).eval ⟨b, hb⟩ = 0) : vanishingStalkIdeal (affine ℂ n).toLocallyRingedSpace D q = (Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine ℂ n).presheaf.germ U q hq)) (h i))).radical

Rückert's Nullstellensatz at a point q of ℂⁿ for the germs of 𝒜_{ℂⁿ}: if near q the set D is the common zero set of analytic functions h_i on U ∋ q, the germs at q vanishing on D are exactly the radical of the ideal generated by the germs of the h_i (vanishingIdeal_eq_radical of Hironaka/Analytic/Rueckert/Nullstellensatz.lean, transported to the stalk at q by the Taylor isomorphism taylorAffine).

theorem AnalyticSpace.isUnit_map_iff_of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Bijective ⇑f) (x : R) : IsUnit (f x) ↔ IsUnit x

A bijective ring homomorphism preserves and detects units.

theorem AnalyticSpace.vanishingStalkIdeal_cosupport_eq_radical_analyticSpaceOfOpen {n : ℕ} (G : TopologicalSpace.Opens (Kn ℂ n)) (J : Manifold.IdealSheaf (analyticSpaceOfOpen ℂ n G).𝒪) (q : ↑↑(analyticSpaceOfOpen ℂ n G).toPresheafedSpace) : vanishingStalkIdeal (analyticSpaceOfOpen ℂ n G).toLocallyRingedSpace J.support q = (J.stalkIdeal q).radical

Rückert's Nullstellensatz on (G, 𝒜_G): the germs at q vanishing on the support of an ideal sheaf J of finite type are the radical of J_q (transport of the affine form along the open immersion (G, 𝒜_G) ⟶ (ℂⁿ, 𝒜), whose stalk maps are isomorphisms).

theorem AnalyticSpace.vanishingStalkIdeal_cosupport_eq_radical_quotient (Y : AlgebraicGeometry.LocallyRingedSpace) (I : Manifold.IdealSheaf Y.𝒪) (J' : Manifold.IdealSheaf (QuotientSpace.quotientSpace Y I).𝒪) (z : ↑(QuotientSpace.quotientSpace Y I).toTopCat) (hY : vanishingStalkIdeal Y (QuotientSpace.liftIdeal Y I J').support ↑z = ((QuotientSpace.liftIdeal Y I J').stalkIdeal ↑z).radical) : vanishingStalkIdeal (QuotientSpace.quotientSpace Y I) J'.support z = (J'.stalkIdeal z).radical

The Nullstellensatz descends to a quotient (S(𝒥), 𝒪_Y/𝒥): for an ideal sheaf J' on the quotient, given the Nullstellensatz on Y for its lift, the germs on the quotient vanishing on the support of J' are the radical of J'_z (transport along the closed immersion, whose stalk maps are the surjections 𝒪_{Y,z} → 𝒪_{Y,z}/𝒥_z).

theorem AnalyticSpace.vanishingStalkIdeal_cosupport_eq_radical (X : AnalyticSpace ℂ) (J : Manifold.IdealSheaf X.𝒪) (y : ↑↑X.toPresheafedSpace) : vanishingStalkIdeal X.toLocallyRingedSpace J.support y = (J.stalkIdeal y).radical

Rückert's Nullstellensatz on an analytic ℂ-space [GR84, Ch. 4, §1]: the germs at y vanishing on the support of an ideal sheaf J are exactly the radical of J_y. Through a chart X|U ≅ (S(𝓘), 𝒜_G/𝓘) and the transport of ideal sheaves (restrictIdeal, comap, liftIdeal), the statement descends from (G, 𝒜_G).