The decomposition 𝓘 = M(𝓘) · N(𝓘) as ideal sheaves

The stalkwise statements of BMO/Split.lean and BMO/SplitOrder.lean lifted to ideal sheaves: the containment 𝓘 ≤ M(𝓘) and the identity M(𝓘) · N(𝓘) = 𝓘 of [Kol07, Definition–Lemma 110], together with the elementary facts that products and powers of ideal sheaves that are nonzero at every point are again nonzero at every point (the stalks of the structure sheaf are domains), and that a factor of such a product is nonzero at every point. These are the forms in which Step 1 of the proof of [Kol07, Theorem 107] compares the nonmonomial part of a marked transform with the transform of the nonmonomial part (BMO/Step1Transform.lean, BMO/Step1PerBlowUp.lean).

theorem Hironaka.Manifold.BMO.le_monomialPart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : I ≤ monomialPart F hF I

The ideal 𝓘 is contained in its monomial part M(𝓘) as ideal sheaves, the sheaf-level form of stalkIdeal_le_monomialPart; the counterpart of le_nonmonomialPart on the other side of the decomposition 𝓘 = M(𝓘) · N(𝓘).

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

The decomposition M(𝓘) · N(𝓘) = 𝓘 of [Kol07, Definition–Lemma 110] as an identity of ideal sheaves: the stalk of a product of ideal sheaves is the product of the stalks, and stalkwise the identity is stalkIdeal_monomialPart_mul_nonmonomialPart.

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_mul {𝕜 : 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] (I J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : I.IsNonzeroEverywhere) (hJ : J.IsNonzeroEverywhere) : (I * J).IsNonzeroEverywhere

The product of two ideal sheaves that are nonzero at every point is nonzero at every point: the stalks of the structure sheaf are domains, so a product of stalks is zero only if a factor is.

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_pow {𝕜 : 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] (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : I.IsNonzeroEverywhere) (k : ℕ) : (I ^ k).IsNonzeroEverywhere

A power of an ideal sheaf that is nonzero at every point is nonzero at every point (the zeroth power is the unit ideal).

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_of_mul_right {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {I J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} (h : (I * J).IsNonzeroEverywhere) : J.IsNonzeroEverywhere

A right factor of a product that is nonzero at every point is nonzero at every point: a zero stalk of J would make the stalk of I · J zero. This lets a product of monomial factors be peeled off one factor at a time while the remaining product stays nonzero.

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_of_mul_left {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {I J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} (h : (I * J).IsNonzeroEverywhere) : I.IsNonzeroEverywhere

A left factor of a product that is nonzero at every point is nonzero at every point.