Ideal sheaves with a zero stalk on a connected manifold

On an analytic manifold, the set of points at which an ideal sheaf J has zero stalk is clopen: open because the local generators vanish near a point with zero stalk (isOpen_setOf_stalkIdeal_eq_bot), closed by the identity theorem applied in a chart ball to a section with nonzero germ (isClosed_setOf_stalkIdeal_eq_bot). So on a connected manifold one zero stalk forces J = 0 (eq_bot_of_isPreconnected), and "nonzero everywhere" is "nonzero somewhere" (isNonzeroEverywhere_iff_exists): Hironaka's "coherent sheaf of non-zero ideals" [Hir64, Main Theorem II''(N), p. 158] and Kollár's "ideal sheaf that is nonzero on every irreducible component" [Kol07, Definition 31] agree on a connected manifold. The clopen description is used to run the resolution componentwise (Hironaka/Resolution/Analytic/OrderReduction/FirstStep.lean).

theorem Manifold.IdealSheaf.germ_eq_zero_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {U : TopologicalSpace.Opens M} {a : M} (ha : a ∈ U) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a ha)) f = 0 ↔ extendSection 𝕜 E f =ᶠ[nhds a] 0

A germ of a section vanishes iff the section vanishes near the point.

theorem Manifold.IdealSheaf.isOpen_setOf_stalkIdeal_eq_bot {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (J : IdealSheaf (structureSheaf 𝕜 E M)) : IsOpen {a : M | J.stalkIdeal a = ⊥}

The set of points with zero stalk is open (the generators vanish near a point with zero stalk).

theorem Manifold.IdealSheaf.isClosed_setOf_stalkIdeal_eq_bot {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (J : IdealSheaf (structureSheaf 𝕜 E M)) : IsClosed {a : M | J.stalkIdeal a = ⊥}

The identity theorem: the set of points with zero stalk is closed — a section with a nonzero germ at b has nonzero germs on a chart ball around b.

theorem Manifold.IdealSheaf.isClopen_setOf_stalkIdeal_eq_bot {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (J : IdealSheaf (structureSheaf 𝕜 E M)) : IsClopen {a : M | J.stalkIdeal a = ⊥}

The set of points with zero stalk is clopen.

theorem Manifold.IdealSheaf.eq_bot_of_isPreconnected {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (J : IdealSheaf (structureSheaf 𝕜 E M)) [PreconnectedSpace M] {a : M} (h : J.stalkIdeal a = ⊥) : J = ⊥

On a connected manifold, one zero stalk forces J = 0 ([Hir64, Main Theorem II''(N), p. 158]; [Kol07, Definition 31]).

theorem Manifold.IdealSheaf.isNonzeroEverywhere_iff_exists {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (J : IdealSheaf (structureSheaf 𝕜 E M)) [ConnectedSpace M] : J.IsNonzeroEverywhere ↔ ∃ (a : ↑↧M), J.stalkIdeal a ≠ ⊥

On a connected manifold, "nonzero everywhere" is "nonzero somewhere": Hironaka's "sheaf of non-zero ideals" and Kollár's "nonzero on every irreducible component" agree.