The nonmonomial part is nonzero and contains the ideal

Step 1 of the proof of [Kol07, Theorem 107] (item 111) reduces the order of the nonmonomial part N(𝓘) by rounds of order reduction, each at the order d = max-ord N(𝓘). Two elementary consequences of the decomposition 𝓘 = M(𝓘) · N(𝓘) (BMO/SplitOrder.lean) are recorded here: N(𝓘) is nonzero at every point whenever 𝓘 is, since a stalk product M(𝓘)_x · N(𝓘)_x = 𝓘_x ≠ 0 has nonzero factors, so that (M, N(𝓘), E) is a genuine triple; and 𝓘 ⊆ N(𝓘), since M(𝓘)_x · N(𝓘)_x ⊆ N(𝓘)_x. The inclusion is what lets a blow-up sequence of order ≥ d for N(𝓘) be read as one of order ≥ m for (𝓘, m) when m ≤ d.

theorem Hironaka.Manifold.BMO.nonmonomialPart_isNonzeroEverywhere {𝕜 : 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)) (hI : I.IsNonzeroEverywhere) : (nonmonomialPart F hF I).IsNonzeroEverywhere

The nonmonomial part N(𝓘) is nonzero at every point when 𝓘 is: from the decomposition M(𝓘)_x · N(𝓘)_x = 𝓘_x, a factor of a nonzero product is nonzero. Hence N(𝓘) is the ideal of a genuine triple (BMO/NonmonomialTriple.lean).

theorem Hironaka.Manifold.BMO.stalkIdeal_le_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) : I.stalkIdeal x ≤ (nonmonomialPart F hF I).stalkIdeal x

At every stalk the ideal 𝓘 is contained in its nonmonomial part N(𝓘): from 𝓘_x = M(𝓘)_x · N(𝓘)_x and M(𝓘)_x · N(𝓘)_x ⊆ N(𝓘)_x. Consequently a centre along which N(𝓘) has order ≥ d is one along which 𝓘 has order ≥ d, which is how Step 1 of the proof of [Kol07, Theorem 107] reads a blow-up sequence for N(𝓘) as one for (𝓘, m).

theorem Hironaka.Manifold.BMO.le_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)) : I ≤ nonmonomialPart F hF I

The inclusion 𝓘 ≤ N(𝓘) as ideal sheaves, the sheaf-level form of stalkIdeal_le_nonmonomialPart.