The Jacobian ideal times a boundary monomial is a normal-crossings divisor

Bierstone–Milman's sentence after Theorem 1.10: if J ⊂ 𝒪_{M_k} is the ideal generated by the Jacobian determinant of σ, then J · σ⁻¹(I) is a normal-crossings divisor [BM97, Theorem 1.10, the sentence after it]. Two tools for that clause: at a point of a manifold carrying a hypersurface family G, two ideal sheaves whose stalks are monomials in the vanishing ideals of members of G through the point have a product of the same form (the index sets unite, the exponents add; exists_prod_pow_vanishingStalk_mul), and when G is snc and the Jacobian stalk of σ and the stalk of J are such monomials at every point, jacobianIdeal σ · J is a normal-crossings divisor (isNormalCrossingsDivisor_jacobianIdeal_mul_of_forall_monomial, through isNormalCrossingsDivisor_of_forall_monomial: the centred coordinates of an snc chart are a regular system of parameters). The stalks of the Jacobian ideal are the jacobianStalks (jacobianIdeal_stalkIdeal). Used for the Jacobian clause of the principalization theorem (Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean).

theorem Hironaka.Manifold.exists_prod_pow_vanishingStalk_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (G : Manifold.HypersurfaceFamily X.carrier) (J K : X.IdealSheaf) (x : X.carrier) (hJ : ∃ (s : Finset G.ι) (α : G.ι → ℕ), (∀ j ∈ s, x ∈ G.hyp j) ∧ Manifold.IdealSheaf.stalkIdeal J x = ∏ j ∈ s, Manifold.vanishingStalk (G.hyp j) x ^ α j) (hK : ∃ (s : Finset G.ι) (α : G.ι → ℕ), (∀ j ∈ s, x ∈ G.hyp j) ∧ Manifold.IdealSheaf.stalkIdeal K x = ∏ j ∈ s, Manifold.vanishingStalk (G.hyp j) x ^ α j) : ∃ (s : Finset G.ι) (α : G.ι → ℕ), (∀ j ∈ s, x ∈ G.hyp j) ∧ Manifold.IdealSheaf.stalkIdeal (J * K) x = ∏ j ∈ s, Manifold.vanishingStalk (G.hyp j) x ^ α j

The product of two boundary monomials of one hypersurface family at a point is a boundary monomial of the same family: the index sets unite and the exponents add (an exponent extended by 0 off its index set).

theorem Hironaka.Manifold.isNormalCrossingsDivisor_jacobianIdeal_mul_of_forall_monomial {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {X X' : AnalyticManifold 𝕜 E} (σ : AnalyticMap X' X) (G : Manifold.HypersurfaceFamily X'.carrier) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (J : X'.IdealSheaf) (hσ : ∀ (x : X'.carrier), ∃ (s : Finset G.ι) (h : G.ι → ℕ), (∀ j ∈ s, x ∈ G.hyp j) ∧ Manifold.jacobianStalk (⇑σ) x = ∏ j ∈ s, Manifold.vanishingStalk (G.hyp j) x ^ h j) (hJ : ∀ (x : X'.carrier), ∃ (s : Finset G.ι) (α : G.ι → ℕ), (∀ j ∈ s, x ∈ G.hyp j) ∧ Manifold.IdealSheaf.stalkIdeal J x = ∏ j ∈ s, Manifold.vanishingStalk (G.hyp j) x ^ α j) : (σ.jacobianIdeal * J).IsNormalCrossingsDivisor

If the Jacobian stalk of σ and the stalk of J are, at every point, monomials in the vanishing ideals of members of the snc family G through the point, then jacobianIdeal σ · J is a normal-crossings divisor [BM97, Theorem 1.10, the sentence after it].