A normal-crossings divisor is a unit times a monomial in analytic coordinates

Bierstone–Milman's normal-crossings divisor [BM97, Theorem 1.10] is stated on stalks (IdealSheaf.IsNormalCrossingsDivisor): at every point x the stalk of the ideal sheaf is generated by a monomial ∏ z_i^{α_i} in a regular system of parameters z of 𝒪_{M,x}. This module reads it as a statement about functions, in one chart for several functions at once: there is a chart at x such that every germ s dividing the monomial, with function germ F, is near x, in the coordinates y of the chart, F = u · y^β with u analytic and u(x) ≠ 0 (IdealSheaf.IsNormalCrossingsDivisor.exists_chart_forall_le_span). For a product J = J₁ J₂ of principal ideal sheaves which is a normal-crossings divisor, the generators of J₁ and J₂ both divide the monomial, so both are monomials times units in the same coordinates: this is how the pull-back of an ideal and the Jacobian determinant of a principalization are read in one chart.

The proof has three steps.

• The parameters are coordinates. The z_i have linearly independent classes in 𝔪_x/𝔪_x² (IsRegularLocalRing.linearIndependent_toCotangent_of_span_eq), so representatives of them have linearly independent differentials at x and vanish there, and the chart-extension theorem (exists_chart_extending, the analytic inverse function theorem) completes them to a chart e of the maximal atlas centred at x: z_i = y_{σ i} near x for an injection σ of the indices into the coordinates. In particular each z_i is prime (prime_coord_of_eq_zero).
• A divisor of the monomial is a monomial times a unit. The stalk is a unique factorization domain (uniqueFactorizationMonoid_stalk_of_chart), and a prime factor of a divisor of ∏ z_i^{α_i} is associated to some z_i (exists_associated_prod_pow_of_dvd_prod_pow), so s = (∏ z_i^{γ_i}) · w with w a unit.
• In functions. A unit germ is the germ of an analytic function that does not vanish at x (mem_maximalIdeal_iff_eval), and the monomial ∏_i y_{σ i}^{γ_i} is ∏_j y_j^{β_j} with β the extension of γ by zero along σ (prod_pow_extend_embedding).

theorem Manifold.prod_pow_extend_embedding {n : ℕ} {R : Type u_2} [CommMonoid R] {m : ℕ} (σ : Fin m ↪ Fin n) (f : Fin n → R) (α : Fin m → ℕ) : ∏ j : Fin n, f j ^ Function.extend (⇑σ) α 0 j = ∏ i : Fin m, f (σ i) ^ α i

A product over the indices i of f (σ i) ^ α i is the product over all j of f j ^ β j, with β the extension of α by zero along the injection σ. Not in the sources; bookkeeping for the monomial in a chart extending a regular system of parameters.

theorem Manifold.exists_associated_prod_pow_of_dvd_prod_pow {R : Type u_2} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {m : ℕ} {p : Fin m → R} (hp : ∀ (i : Fin m), Prime (p i)) (α : Fin m → ℕ) {a : R} (ha : a ∣ ∏ i : Fin m, p i ^ α i) : ∃ (γ : Fin m → ℕ), Associated (∏ i : Fin m, p i ^ γ i) a

In a unique factorization domain, a divisor of a product of powers of primes is associated to a product of powers of the same primes. Not in the sources; the factorization step of the monomial form of the factors of a normal-crossings divisor.

theorem Manifold.exists_chart_forall_dvd_prod_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (ψ : E ≃L[𝕜] Fin n → 𝕜) {x : M} {m : ℕ} {z : Fin m → ↑((structureSheaf 𝕜 E M).presheaf.stalk x)} (hz : IsLocalRing.IsRegularSystemOfParameters z) (α : Fin m → ℕ) : ∃ e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M, x ∈ e.source ∧ ∀ (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk x)) (F : M → 𝕜), s ∣ ∏ i : Fin m, z i ^ α i → (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M x) s = ↑F → ∃ (β : Fin n → ℕ) (u : M → 𝕜), ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ u x ∧ u x ≠ 0 ∧ ∀ᶠ (y : M) in nhds x, F y = u y * ∏ j : Fin n, ψ (↑e y) j ^ β j

The divisors of a monomial in a regular system of parameters, in coordinates. Let z be a regular system of parameters of 𝒪_{M,x} and α exponents. There is a chart e of the maximal atlas at x such that every germ s dividing the monomial ∏ z_i^{α_i}, with function germ F, is in the coordinates y = ψ ∘ e a monomial times a unit: near x, F = u · ∏_j y_j^{β_j} with u analytic at x and u x ≠ 0. The chart does not depend on s.

theorem AnalyticManifold.IdealSheaf.IsNormalCrossingsDivisor.exists_chart_forall_le_span {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] Fin n → 𝕜) {J : M.IdealSheaf} (hJ : J.IsNormalCrossingsDivisor) (x : M.carrier) : ∃ e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier, x ∈ e.source ∧ ∀ (s : stalkRing M x) (F : M.carrier → 𝕜), Manifold.IdealSheaf.stalkIdeal J x ≤ Ideal.span {s} → (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M.carrier x) s = ↑F → ∃ (β : Fin n → ℕ) (u : M.carrier → 𝕜), ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ u x ∧ u x ≠ 0 ∧ ∀ᶠ (y : M.carrier) in nhds x, F y = u y * ∏ j : Fin n, ψ (↑e y) j ^ β j

A normal-crossings divisor and the generators of the principal ideals containing it are, in suitable analytic coordinates, units times monomials (the reading of [BM97, Theorem 1.10] "generated locally by a monomial in suitable coordinates" as functions). If J is a normal-crossings divisor and x a point, there is a chart e of the maximal atlas at x such that every germ s whose principal ideal contains the stalk J_x, with function germ F, is near x, in the coordinates y = ψ ∘ e, of the form F = u · ∏_j y_j^{β_j} with u analytic at x and u x ≠ 0. Applied to a generator of J_x, and to the generators of principal ideals of which J_x is a product, it puts them all in monomial form in the same coordinates.