The nonmonomial part of an ideal sheaf

The decomposition I = M(I) · N(I) of [Kol07, Definition–Lemma 110] defines the nonmonomial part N(I) of an ideal sheaf I with respect to a boundary family: the part of I left after the monomial part M(I) (BMO/MonomialPart.lean) has been divided out, that is, the ideal colon N(I) = I : M(I). This file assembles N(I) as an ideal sheaf on an analytic manifold.

The stalk of N(I) at x is the colon I_x : M(I)_x. It has local generators because M(I) is locally generated by a single non-zero-divisor (exists_nonZeroDivisor_stalkIdeal_monomialPart, BMO/Split.lean) and I ⊆ M(I) stalkwise (stalkIdeal_le_monomialPart): the general colon lemma HasLocalRegularGenerator.hasLocalGenerators_colon of BMO/ColonLocalPrincipal.lean then divides the local generators of I by the generator of M(I). The analytic counterpart of Hironaka.BMO.nonmonomialPart.

noncomputable def Hironaka.Manifold.BMO.nonmonomialPart {𝕜 : 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] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)

The nonmonomial part N(I) = I : M(I) of I with respect to the boundary family F: the ideal sheaf whose stalk at x is the colon of I_x by the stalk of the monomial part ([Kol07, Definition–Lemma 110]). Its local generators come from dividing those of I by the local non-zero-divisor generator of M(I). The analytic counterpart of Hironaka.BMO.nonmonomialPart.

Equations

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

@[simp]

theorem Hironaka.Manifold.BMO.stalkIdeal_nonmonomialPart {𝕜 : 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] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (x : M) : (nonmonomialPart F hF I).stalkIdeal x = Submodule.colon (I.stalkIdeal x) ↑((monomialPart F hF I).stalkIdeal x)

The stalk of the nonmonomial part N(I) at x is the colon I_x : M(I)_x.