The monomial part is locally principal

The decomposition I = M(I) · N(I) of [Kol07, Definition–Lemma 110] rests on the monomial part M(I) being an invertible ideal sheaf. This file proves the local form of that statement on an analytic manifold: at every point x the stalk M(I)_x is the principal ideal generated by a nonzero element of the domain 𝒪_{M,x}, namely the monomial ∏_D z_D^{ord_D I} over the components D through x, where z_D is the coordinate cutting out D in a chart adapted to the boundary family. The file also proves the containment I_x ⊆ M(I)_x, which the colon N(I) = I : M(I) needs: I vanishes to order ≥ ord_D I along each component D through x, the coordinates of distinct components are pairwise non-associated primes of the stalk, and so their product of powers divides every element of I_x.

Two general facts sit beside their use here: prod_pow_dvd_of_prime_of_not_dvd (divisibility by a product of powers of pairwise non-dividing primes in a domain) and nhds_subtype_map_eq. The analytic counterpart of Hironaka.BMO.isInvertible_monomialPart.

theorem prod_pow_dvd_of_prime_of_not_dvd {R : Type u_1} [CommRing R] [IsDomain R] {ι : Type u_2} (s : Finset ι) (p : ι → R) (e : ι → ℕ) (hp : ∀ i ∈ s, Prime (p i)) (hnd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ¬p i ∣ p j) {z : R} (hz : ∀ i ∈ s, p i ^ e i ∣ z) : ∏ i ∈ s, p i ^ e i ∣ z

In a domain, if z is divisible by each p i ^ e i over a finite set of pairwise non-dividing primes p i, then it is divisible by their product. The prime-power form of IsLocalRing.prod_dvd_of_prime_of_not_dvd; not in the sources.

theorem Hironaka.Manifold.BMO.stalkIdeal_monomialPart_eq_span {𝕜 : 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) : ∃ (g : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk x)), g ≠ 0 ∧ (monomialPart F hF I).stalkIdeal x = Ideal.span {g}

The stalk of the monomial part M(I) at x is the principal ideal of a nonzero element of the domain 𝒪_{M,x}, namely the monomial ∏_D z_D^{ord_D I} over the components D through x, z_D the adapted coordinate of D. This is the local content of "M(I) is invertible" in [Kol07, Definition–Lemma 110].

theorem Hironaka.Manifold.BMO.exists_nonZeroDivisor_stalkIdeal_monomialPart {𝕜 : 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) : ∃ g ∈ nonZeroDivisors ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk x), (monomialPart F hF I).stalkIdeal x = Ideal.span {g}

The stalk of the monomial part M(I) at x is generated by a single non-zero-divisor (a nonzero element of the domain 𝒪_{M,x}). This is the hypothesis under which the colon I : M(I) has local generators (BMO/ColonLocalPrincipal.lean).

theorem Hironaka.Manifold.BMO.stalkIdeal_le_componentFactor {𝕜 : 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) : I.stalkIdeal x ≤ (componentFactor F hF I i).stalkIdeal x

At a point x of the component D = i, the ideal I vanishes to order at least ord_D I along D, so I_x ⊆ 𝓘_D^{ord_D I}: the order of I along D is constant on the connected component and bounded by its value at x. One factor of the containment I ⊆ M(I).

theorem Hironaka.Manifold.BMO.active_component_injective_fst {M : Type u} [TopologicalSpace M] (F : Manifold.HypersurfaceFamily M) {i i' : ComponentIndex F} {x : M} (hi : x ∈ componentSet F i) (hi' : x ∈ componentSet F i') (hfst : i.fst = i'.fst) : i = i'

A point of a member E^j lies in exactly one connected component of E^j: two components of the same member through a common point coincide. This transfers the pairwise coprimality of the coordinates of distinct members to the components through a point.

theorem Hironaka.Manifold.BMO.nhds_subtype_map_eq {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} (hx : x ∈ s) : Filter.map Subtype.val (nhds ⟨x, hx⟩) = nhdsWithin x s

The neighbourhood filter within a set s at x ∈ s is the image of the neighbourhood filter of the subtype at ⟨x, hx⟩, stated with the base point spelled as x : X so that it rewrites directly.

theorem Hironaka.Manifold.BMO.componentIdeal_stalkIdeal_eq {𝕜 : 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).stalkIdeal x = ⋯.idealSheaf.stalkIdeal x

Near a point x of the component D = i, the reduced ideal sheaf of D and the reduced ideal sheaf of the whole member E^{i.1} have the same stalk: the component is a connected component of the member, hence open in it (a closed submanifold is locally connected), so the two sets have the same neighbourhood filter at x, and a germ lies in either stalk ideal exactly when its section vanishes on the set near x. This carries the member-indexed coordinates of a chart adapted to the boundary to the component-indexed factors of M(I).

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

The stalk containment I_x ⊆ M(I)_x, the hypothesis of the colon N(I) = I : M(I) in [Kol07, Definition–Lemma 110]. In a chart adapted to the boundary at x, each component D through x has 𝓘_D generated by the coordinate z_D of its member (componentIdeal_stalkIdeal_eq), so M(I)_x is generated by ∏_D z_D^{ord_D I}; each factor z_D^{ord_D I} divides every element of I_x (stalkIdeal_le_componentFactor), and the coordinates of distinct components are pairwise non-dividing primes, so the product divides as well (prod_pow_dvd_of_prime_of_not_dvd).