The principal ideal sheaf of a global analytic function

The ideal sheaf (t) generated by one global section t of the sheaf of analytic functions on an analytic manifold (IdealSheaf.principal t): its stalk at x is the principal ideal generated by the germ of t (stalkIdeal_principal), and this stalk is the unit ideal exactly where t does not vanish (stalkIdeal_principal_eq_top_iff: a germ is a unit iff its value is nonzero), so the support of (t) is the zero set of t. The ideal sheaf of a single function, to which the resolution theorems are applied to monomialize the function (Watanabe's (f) [Wat09, Theorem 2.3]; the monomialization of Hironaka/Resolution/Standard/Analytic.lean).

noncomputable def Manifold.IdealSheaf.principal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (t : ↑((structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op ⊤))) : M.IdealSheaf

The principal ideal sheaf (t) of a global section t of 𝒪_M (IdealSheaf.ofStalks): the stalks span {germ_x t}, which have the local generator t (hasLocalGenerators_span_germ_top).

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.IdealSheaf.stalkIdeal_principal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (t : ↑((structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op ⊤))) (x : M.carrier) : stalkIdeal (principal t) x = Ideal.span {(CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M.carrier).presheaf.germ ⊤ x ⋯)) t}

The stalk of (t) at x is the principal ideal generated by the germ of t at x.

theorem Manifold.IdealSheaf.stalkIdeal_principal_eq_top_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (t : ↑((structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op ⊤))) (x : M.carrier) : stalkIdeal (principal t) x = ⊤ ↔ ↑t ⟨x, ⋯⟩ ≠ 0

The stalk of (t) at x is the unit ideal iff t x ≠ 0 (a germ is a unit iff its value is nonzero: 𝔪_x = ker ev_x).