The order along a smooth hypersurface is a valuation; the exponents of the monomial part

The order ord_D J of an ideal sheaf J along a subvariety D is the largest p with J ⊆ 𝓘_D^p at the point ([Kol07, Definition 47]; [BM97, §3] in the analytic setting). This file proves that at a point where the ideal of D is generated by a prime element c of the stalk, a domain, the order along D is the c-adic valuation of ideals: additive on products (IdealSheaf.ordAlongIdeal_mul_of_stalkIdeal_eq_span), with the forms for powers and finite products, ord_D D = 1, and ord_D J = ⊤ exactly when the stalk of J is zero (Krull's intersection theorem in the Noetherian local stalk). The inequality ord_D (J·K) ≥ ord_D J + ord_D K is elementary; for the other inequality, elements f ∈ J, g ∈ K of exact c-multiplicities k, l have f g of exact multiplicity k + l. Along a smooth hypersurface S of an analytic manifold these hold at every point of S, where the coordinate adapted to S is a prime element of the factorial stalk; off S every order along S is ⊤.

For a boundary family F with simple normal crossings and the decomposition 𝓘 = M(𝓘) · N(𝓘) of [Kol07, Definition–Lemma 110] (BMO/MonomialPart.lean, BMO/NonmonomialPart.lean), the consequences are: the exponent ord_D 𝓘 of a component D can be read at any point of D (componentExponent_eq_toNat_ordAlongIdeal); ord_D M(𝓘) = ord_D 𝓘 at every point of D; the exponents of the nonmonomial part all vanish (componentExponent_nonmonomialPart_eq_zero, the statement "cosupp N(I) does not contain any of the Eⁱ" of Kollár's lemma, component by component), so M(N(𝓘)) = ⊤ and N(N(𝓘)) = N(𝓘); and the exponents are additive on products of ideal sheaves that are nonzero at every point, so multiplying by a power of the ideal of a component raises exactly that component's exponent: the monomial part absorbs monomial factors (monomialPart_componentIdeal_pow_mul) and the nonmonomial part ignores them (nonmonomialPart_componentIdeal_pow_mul), which is the one-component form of the remark of Kol07, 111, Step 1 that an ideal of boundary divisors changes only the monomial part.

A. Ring lemmas: exact multiplicity and the c-adic filtration

theorem Ideal.exists_mem_emultiplicity_eq {R : Type u_1} [CommRing R] {c : R} {J : Ideal R} {k : ℕ} (h₁ : J ≤ span {c} ^ k) (h₂ : ¬J ≤ span {c} ^ (k + 1)) : ∃ f ∈ J, emultiplicity c f = ↑k

If J ⊆ (c)^k but J ⊄ (c)^(k+1), some element of J has c-multiplicity exactly k.

B. The order along a divisor at a point: generic stalk-level facts

theorem Manifold.IdealSheaf.ordAlongIdeal_of_stalkIdeal_eq_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) (a : ↑X) (hD : D.stalkIdeal a = ⊤) : D.ordAlongIdeal J a = ⊤

Where the stalk of D is the unit ideal (off the divisor), every order along D is ⊤.

theorem Manifold.IdealSheaf.ordAlongIdeal_eq_zero_of_stalkIdeal_eq_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) (a : ↑X) (hJ : J.stalkIdeal a = ⊤) (hD : D.stalkIdeal a ≠ ⊤) : D.ordAlongIdeal J a = 0

An ideal sheaf whose stalk at a is the unit ideal (for instance the unit ideal sheaf) has order 0 along a divisor whose stalk at a is proper.

theorem Manifold.IdealSheaf.ordAlongIdeal_eq_zero_of_stalkIdeal_eq_span_of_not_dvd {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) (a : ↑X) {c d : ↑(𝒪.presheaf.stalk a)} (hD : D.stalkIdeal a = Ideal.span {c}) (hJ : J.stalkIdeal a = Ideal.span {d}) (hcd : ¬c ∣ d) : D.ordAlongIdeal J a = 0

Along a divisor whose stalk is (c), an ideal sheaf whose stalk is (d) has order 0 when c ∤ d.

theorem Manifold.IdealSheaf.ordAlongIdeal_self_of_stalkIdeal_eq_span {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) (a : ↑X) [hdom : IsDomain ↑(𝒪.presheaf.stalk a)] {c : ↑(𝒪.presheaf.stalk a)} (hD : D.stalkIdeal a = Ideal.span {c}) (hc : Prime c) : D.ordAlongIdeal D a = 1

Along a divisor whose stalk is the prime (c) of the domain stalk, the divisor itself has order exactly 1: c ∉ (c)², since c is neither zero nor a unit.

theorem Manifold.IdealSheaf.ordAlongIdeal_mul_of_stalkIdeal_eq_span {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) (a : ↑X) [hdom : IsDomain ↑(𝒪.presheaf.stalk a)] {c : ↑(𝒪.presheaf.stalk a)} (hD : D.stalkIdeal a = Ideal.span {c}) (hc : Prime c) (J K : IdealSheaf 𝒪) : D.ordAlongIdeal (J * K) a = D.ordAlongIdeal J a + D.ordAlongIdeal K a

The order along a divisor is a valuation: at a point where the stalk of the divisor is the prime (c) of the domain stalk, ord_D (J · K) = ord_D J + ord_D K in ℕ∞. The inequality ≥ is le_ordAlongIdeal_mul; for ≤, elements f ∈ J_a, g ∈ K_a of exact c-multiplicities k, l (Ideal.exists_mem_emultiplicity_eq) have f g of multiplicity k + l (emultiplicity_mul), so f g ∈ (J K)_a is not in (c)^(k+l+1); the cases with a ⊤ are those of a zero stalk.

theorem Manifold.IdealSheaf.ordAlongIdeal_pow_of_stalkIdeal_eq_span {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) (a : ↑X) [hdom : IsDomain ↑(𝒪.presheaf.stalk a)] {c : ↑(𝒪.presheaf.stalk a)} (hD : D.stalkIdeal a = Ideal.span {c}) (hc : Prime c) (J : IdealSheaf 𝒪) (s : ℕ) : D.ordAlongIdeal (J ^ s) a = ↑s * D.ordAlongIdeal J a

Along a divisor whose stalk is a prime principal ideal, the order of a power is the multiple of the order (in ℕ∞, where 0 · ⊤ = 0 and the unit ideal sheaf has order 0).

theorem Manifold.IdealSheaf.ordAlongIdeal_finset_prod_of_stalkIdeal_eq_span {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) (a : ↑X) [hdom : IsDomain ↑(𝒪.presheaf.stalk a)] {c : ↑(𝒪.presheaf.stalk a)} (hD : D.stalkIdeal a = Ideal.span {c}) (hc : Prime c) {ι : Type u_1} (F : Finset ι) (G : ι → IdealSheaf 𝒪) : D.ordAlongIdeal (∏ i ∈ F, G i) a = ∑ i ∈ F, D.ordAlongIdeal (G i) a

Along a divisor whose stalk is a prime principal ideal, the order of a finite product is the sum of the orders.

theorem Manifold.IdealSheaf.ordAlongIdeal_eq_top_iff_of_stalkIdeal_eq_span {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) (a : ↑X) [hnoeth : IsNoetherianRing ↑(𝒪.presheaf.stalk a)] [hloc : IsLocalRing ↑(𝒪.presheaf.stalk a)] {c : ↑(𝒪.presheaf.stalk a)} (hD : D.stalkIdeal a = Ideal.span {c}) (hc : ¬IsUnit c) : D.ordAlongIdeal J a = ⊤ ↔ J.stalkIdeal a = ⊥

At a point where the stalk of the divisor is a proper principal ideal (c) of a Noetherian local stalk, the order along the divisor is ⊤ exactly when the stalk of the ideal sheaf is zero: Krull's intersection theorem, ⋂ₚ (c)^p = 0.

C. Along a smooth hypersurface

theorem Manifold.IsClosedSubmanifold.exists_stalkIdeal_idealSheaf_eq_span_prime {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {x : M} (hx : x ∈ S) : ∃ (c : ↑((structureSheaf 𝕜 E M).presheaf.stalk x)), Prime c ∧ hS.idealSheaf.stalkIdeal x = Ideal.span {c}

At a point of a smooth hypersurface S, the stalk of the ideal sheaf 𝓘_S is generated by a prime element of the stalk, the coordinate of a chart adapted to S that vanishes along S.

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_ne_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {x : M} (hx : x ∈ S) : hS.idealSheaf.stalkIdeal x ≠ ⊤

At a point of the hypersurface the stalk of 𝓘_S is a proper ideal.

theorem Manifold.IsClosedSubmanifold.ordAlongIdeal_idealSheaf_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) {x : M} (hx : x ∉ S) : hS.idealSheaf.ordAlongIdeal J x = ⊤

Off the hypersurface every order along it is ⊤.

theorem Manifold.IsClosedSubmanifold.ordAlongIdeal_idealSheaf_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {x : M} (hx : x ∈ S) : hS.idealSheaf.ordAlongIdeal 1 x = 0

At a point of the hypersurface the unit ideal sheaf has order 0 along it.

theorem Manifold.IsClosedSubmanifold.ordAlongIdeal_idealSheaf_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (J K : IdealSheaf (structureSheaf 𝕜 E M)) (x : M) : hS.idealSheaf.ordAlongIdeal (J * K) x = hS.idealSheaf.ordAlongIdeal J x + hS.idealSheaf.ordAlongIdeal K x

The order along a smooth hypersurface S is additive on products, at every point of M: on S because the stalk of 𝓘_S is generated by a prime element of the domain stalk (IdealSheaf.ordAlongIdeal_mul_of_stalkIdeal_eq_span), off S because both sides are ⊤.

theorem Manifold.IsClosedSubmanifold.ordAlongIdeal_idealSheaf_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) (s : ℕ) {x : M} (hx : x ∈ S) : hS.idealSheaf.ordAlongIdeal (J ^ s) x = ↑s * hS.idealSheaf.ordAlongIdeal J x

At a point of the hypersurface, the order along it of a power is the multiple of the order. (Off the hypersurface the statement fails for the zeroth power, whose order is ⊤.)

theorem Manifold.IsClosedSubmanifold.ordAlongIdeal_idealSheaf_finset_prod {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {ι : Type u_2} (F : Finset ι) (G : ι → IdealSheaf (structureSheaf 𝕜 E M)) {x : M} (hx : x ∈ S) : hS.idealSheaf.ordAlongIdeal (∏ i ∈ F, G i) x = ∑ i ∈ F, hS.idealSheaf.ordAlongIdeal (G i) x

At a point of the hypersurface, the order along it of a finite product is the sum of the orders.

theorem Manifold.IsClosedSubmanifold.ordAlongIdeal_idealSheaf_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {x : M} (hx : x ∈ S) : hS.idealSheaf.ordAlongIdeal hS.idealSheaf x = 1

A smooth hypersurface has order 1 along itself at each of its points.

theorem Manifold.IsClosedSubmanifold.ordAlongIdeal_idealSheaf_eq_top_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) {x : M} (hx : x ∈ S) : hS.idealSheaf.ordAlongIdeal J x = ⊤ ↔ J.stalkIdeal x = ⊥

At a point of the hypersurface, the order along it is ⊤ exactly when the stalk of the ideal sheaf is zero (Krull's intersection theorem in the Noetherian local stalk).

theorem Manifold.IsClosedSubmanifold.genericOrdAlong_idealSheaf_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (J K : IdealSheaf (structureSheaf 𝕜 E M)) (x : M) : hS.idealSheaf.genericOrdAlong (J * K) x = hS.idealSheaf.genericOrdAlong J x + hS.idealSheaf.genericOrdAlong K x

The generic order along a smooth hypersurface is additive: on S it is the pointwise order, which is constant along the connected components, and off S it is ⊤.

D. The components of the boundary family and the decomposition 𝓘 = M(𝓘)·N(𝓘)

theorem Hironaka.Manifold.BMO.out_mem_componentSet {M : Type u} [TopologicalSpace M] (F : Manifold.HypersurfaceFamily M) (i : ComponentIndex F) : ↑(Quotient.out i.snd) ∈ componentSet F i

The representative point of the component i lies on its component set.

theorem Hironaka.Manifold.BMO.isPreconnected_componentSet {M : Type u} [TopologicalSpace M] (F : Manifold.HypersurfaceFamily M) (i : ComponentIndex F) : IsPreconnected (componentSet F i)

A component set is preconnected, being the image of a connected component of the member.

theorem Hironaka.Manifold.BMO.componentExponent_eq_toNat_ordAlongIdeal {𝕜 : 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 : ComponentIndex F) {x : M} (hx : x ∈ componentSet F i) : componentExponent F hF I i = ((componentIdeal F hF i).ordAlongIdeal I x).toNat

The exponent ord_D 𝓘 of the monomial part at a component D can be read at any point x of D: the generic order is the pointwise order at the representative, and the order along a smooth hypersurface is constant on the connected component.

theorem Hironaka.Manifold.BMO.componentIdeal_ordAlongIdeal_self {𝕜 : 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 : ComponentIndex F) {x : M} (hx : x ∈ componentSet F i) : (componentIdeal F hF i).ordAlongIdeal (componentIdeal F hF i) x = 1

A component has order 1 along itself at each of its points.

theorem Hironaka.Manifold.BMO.componentIdeal_ordAlongIdeal_of_notMem {𝕜 : 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 i' : ComponentIndex F) {x : M} (hx : x ∈ componentSet F i) (hx' : x ∉ componentSet F i') : (componentIdeal F hF i).ordAlongIdeal (componentIdeal F hF i') x = 0

Along a component D, another component D' not passing through the point x has order 0 there, its ideal sheaf being the unit ideal at x.

theorem Hironaka.Manifold.BMO.componentIdeal_ordAlongIdeal_of_ne {𝕜 : 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 i' : ComponentIndex F} (hne : i ≠ i') {x : M} (hx : x ∈ componentSet F i) (hx' : x ∈ componentSet F i') : (componentIdeal F hF i).ordAlongIdeal (componentIdeal F hF i') x = 0

Along a component D, a different component D' through the same point has order 0: in a chart of simple normal crossings at the point ([Kol07, Definition 24]) the two are distinct coordinate hyperplanes, whose coordinates do not divide each other.

theorem Hironaka.Manifold.BMO.ordAlongIdeal_componentIdeal_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 : ComponentIndex F) {x : M} (hx : x ∈ componentSet F i) : (componentIdeal F hF i).ordAlongIdeal (monomialPart F hF I) x = ↑(componentExponent F hF I i)

The order of the monomial part along a component is the exponent: at every point x of D, ord_D M(𝓘) = ord_D 𝓘. The stalk of M(𝓘) is the product of the factors 𝓘_{D'}^{e_{D'}} of the components through x, the order along D is additive, ord_D 𝓘_D = 1, and ord_D 𝓘_{D'} = 0 for the other components.

theorem Hironaka.Manifold.BMO.componentExponent_nonmonomialPart_eq_zero {𝕜 : 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 : ComponentIndex F) : componentExponent F hF (nonmonomialPart F hF I) i = 0

The exponents of the nonmonomial part vanish: at the representative point of the component D, ord_D 𝓘 = ord_D M(𝓘) + ord_D N(𝓘) = e_D + ord_D N(𝓘) by the decomposition M(𝓘) · N(𝓘) = 𝓘 and additivity; if ord_D 𝓘 = ⊤ then e_D = 0 and ord_D N(𝓘) = ⊤, otherwise cancellation gives ord_D N(𝓘) = 0; in both cases the exponent is 0. This is the clause of [Kol07, Definition–Lemma 110] that the cosupport of N(I) contains no boundary divisor, taken component by component.

theorem Hironaka.Manifold.BMO.monomialPart_nonmonomialPart_eq_top {𝕜 : 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 (nonmonomialPart F hF I) = ⊤

The monomial part of the nonmonomial part is the unit ideal sheaf, M(N(𝓘)) = ⊤: every exponent of N(𝓘) is 0.

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

The nonmonomial part is idempotent, N(N(𝓘)) = N(𝓘): the colon by the unit ideal M(N(𝓘)) = ⊤ is the identity. The analytic counterpart of Hironaka.BMO.nonmonomialPart_nonmonomialPart.

E. Exponents of products; the nonmonomial part ignores monomial factors

theorem Hironaka.Manifold.BMO.ordAlongIdeal_componentIdeal_ne_top {𝕜 : 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)) (hI : I.IsNonzeroEverywhere) (i : ComponentIndex F) {x : M} (hx : x ∈ componentSet F i) : (componentIdeal F hF i).ordAlongIdeal I x ≠ ⊤

Along a component, an ideal sheaf that is nonzero at every point has finite order at every point of the component (Krull's intersection theorem).

theorem Hironaka.Manifold.BMO.componentExponent_mul {𝕜 : 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 J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : I.IsNonzeroEverywhere) (hJ : J.IsNonzeroEverywhere) (i : ComponentIndex F) : componentExponent F hF (I * J) i = componentExponent F hF I i + componentExponent F hF J i

The component exponents are additive on products of ideal sheaves that are nonzero at every point (the hypotheses exclude the orders ⊤, which toNat would read as 0).

theorem Hironaka.Manifold.BMO.componentExponent_componentIdeal_pow_mul {𝕜 : 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)) (hI : I.IsNonzeroEverywhere) (i : ComponentIndex F) (k : ℕ) : componentExponent F hF (componentIdeal F hF i ^ k * I) i = k + componentExponent F hF I i

Multiplying by the k-th power of the ideal of a component raises that component's exponent by k.

theorem Hironaka.Manifold.BMO.componentExponent_componentIdeal_pow_mul_of_ne {𝕜 : 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 i' : ComponentIndex F} (hne : i ≠ i') (k : ℕ) : componentExponent F hF (componentIdeal F hF i' ^ k * I) i = componentExponent F hF I i

Multiplying by a power of the ideal of another component does not change the exponent: the other component has order 0 along this one at every point, whether or not the two meet there.

theorem Ideal.colon_span_singleton_mul_mul {R : Type u_2} [CommRing R] [IsDomain R] {a : R} (ha : a ≠ 0) (I J : Ideal R) : Submodule.colon (span {a} * I) ↑(span {a} * J) = Submodule.colon I ↑J

In a domain, a nonzero a cancels from both sides of a colon: (a·I : a·J) = (I : J).

theorem Hironaka.Manifold.BMO.monomialPart_componentIdeal_pow_mul {𝕜 : 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)) (hI : I.IsNonzeroEverywhere) (i : ComponentIndex F) (k : ℕ) : monomialPart F hF (componentIdeal F hF i ^ k * I) = componentIdeal F hF i ^ k * monomialPart F hF I

The monomial part absorbs a monomial factor: M(𝓘_D^k · 𝓘) = 𝓘_D^k · M(𝓘) for a component D and 𝓘 nonzero at every point. The exponent at D rises by k and the other exponents are unchanged.

theorem Hironaka.Manifold.BMO.nonmonomialPart_componentIdeal_pow_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] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : I.IsNonzeroEverywhere) (i : ComponentIndex F) (k : ℕ) : nonmonomialPart F hF (componentIdeal F hF i ^ k * I) = nonmonomialPart F hF I

The nonmonomial part ignores a monomial factor: N(𝓘_D^k · 𝓘) = N(𝓘) for a component D and 𝓘 nonzero at every point ([Kol07, 111, Step 1]: multiplying by an ideal of boundary divisors changes only the monomial part). On D the common factor c^k cancels from the colon (Ideal.colon_span_singleton_mul_mul), off D the factor is the unit ideal. The analytic counterpart of Hironaka.BMO.nonmonomialPart_monomial_mul for one component.