The decomposition I = M(I) · N(I) at the stalk

The nonmonomial part N(I) = I : M(I) is defined so that I = M(I) · N(I) ([Kol07, Definition–Lemma 110]). This file proves that identity at every stalk, M(I)_x · N(I)_x = I_x. It is an instance of the ring-theoretic fact that for an ideal I ≤ (g) one has (g) · (I : (g)) = I, applied with (g) = M(I)_x, which is principal (exists_nonZeroDivisor_stalkIdeal_monomialPart) and contains I_x (stalkIdeal_le_monomialPart). The analytic counterpart of Hironaka.BMO.monomialPart_mul_nonmonomialPart.

theorem Ideal.span_singleton_mul_colon_of_le {R : Type u_1} [CommRing R] {g : R} {I : Ideal R} (hle : I ≤ span {g}) : span {g} * Submodule.colon I ↑(span {g}) = I

In a commutative ring, if I ≤ (g) then (g) · (I : (g)) = I. No regularity of g is needed: the invertibility of the monomial part enters the decomposition I = M(I) · N(I) only through the containment I ≤ M(I) and the local principal generator. Not in the sources.

theorem Hironaka.Manifold.BMO.stalkIdeal_monomialPart_mul_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) : (monomialPart F hF I).stalkIdeal x * (nonmonomialPart F hF I).stalkIdeal x = I.stalkIdeal x

At every stalk the monomial part times the nonmonomial part is I: M(I)_x · N(I)_x = I_x ([Kol07, Definition–Lemma 110]). The stalk M(I)_x is principal and contains I_x, so Ideal.span_singleton_mul_colon_of_le applies to the colon N(I)_x = I_x : M(I)_x.