From the pointwise boundary monomial to a normal-crossings divisor

Bierstone–Milman's normal-crossings divisor is "a principal ideal of finite type, generated locally by a monomial in suitable coordinates" [BM97, Theorem 1.10]; the predicate IsNormalCrossingsDivisor asks, at every point, for the stalk to be generated by a monomial in a regular system of parameters. This follows from the pointwise boundary-monomial form of Kollár's formula [Kol07, 72] in an snc chart of the boundary at the point: the chart's coordinates, centred at the point, are a regular system of parameters (maximalIdeal_eq_span_coord', ringKrullDim_stalk_of_chart), the vanishing ideal of a member through the point is generated by its coordinate (IsClosedSubmanifold.vanishingStalk_eq_span_coord, already centred since the member passes through the point), so the product of powers of the vanishing ideals is the ideal generated by the corresponding monomial in the coordinates (isNormalCrossingsDivisor_of_forall_monomial). The support of the ideal sheaf lies in the boundary: off it the monomial is the empty product (support_subset_of_forall_monomial). Used for the normal-crossings clauses of the principalization theorem (JacobianMonomial.lean, Hironaka/Resolution/Analytic/Wlo09/Monomial.lean).

noncomputable def Hironaka.Manifold.chartCentredCoord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {X : AnalyticManifold 𝕜 E} (φ : OpenPartialHomeomorph X.carrier E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ X.carrier) {x : X.carrier} (hx : x ∈ φ.source) (i : Fin n) : ↑((Manifold.structureSheaf 𝕜 E X.carrier).presheaf.stalk x)

The coordinates of a chart, centred at the point x: z_i − z_i(x), the generators of the maximal ideal of the stalk.

Equations

• Hironaka.Manifold.chartCentredCoord ψ φ hφ hx i = Manifold.coord E ψ φ hφ hx i - (Manifold.const 𝕜 E X.carrier x) ((Manifold.eval 𝕜 E X.carrier x) (Manifold.coord E ψ φ hφ hx i))

theorem Hironaka.Manifold.span_range_chartCentredCoord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {X : AnalyticManifold 𝕜 E} (φ : OpenPartialHomeomorph X.carrier E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ X.carrier) {x : X.carrier} (hx : x ∈ φ.source) : Ideal.span (Set.range (chartCentredCoord ψ φ hφ hx)) = IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 E X.carrier).presheaf.stalk x)

The centred coordinates generate the maximal ideal of the stalk.

theorem Hironaka.Manifold.chartCentredCoord_eq_coord_of_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {X : AnalyticManifold 𝕜 E} (φ : OpenPartialHomeomorph X.carrier E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ X.carrier) {x : X.carrier} (hx : x ∈ φ.source) {i : Fin n} (h0 : ψ (↑φ x) i = 0) : chartCentredCoord ψ φ hφ hx i = Manifold.coord E ψ φ hφ hx i

A coordinate vanishing at x is already centred.

theorem Hironaka.Manifold.prod_pow_sum_ite_eq {n : ℕ} {R : Type u_2} [CommMonoid R] {ι : Type u_3} (s : Finset ι) (z : Fin n → R) (cj : ι → Fin n) (α : ι → ℕ) : (∏ i : Fin n, z i ^ ∑ j ∈ s, if cj j = i then α j else 0) = ∏ j ∈ s, z (cj j) ^ α j

The monomial ∏ z_{c j}^{α j} over the members through the point, as a monomial in all the coordinates: the exponent of z_i is the sum of the α j with c j = i (zero off the image).

theorem Hironaka.Manifold.isNormalCrossingsDivisor_of_forall_monomial {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 E} (G : Manifold.HypersurfaceFamily X.carrier) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (J : X.IdealSheaf) (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) : J.IsNormalCrossingsDivisor

An ideal sheaf which is at every point a boundary monomial of the snc family G is a normal-crossings divisor [BM97, Theorem 1.10]: in an snc chart at the point the centred coordinates are a regular system of parameters and the vanishing ideals of the members through the point are generated by their coordinates.

theorem Hironaka.Manifold.support_subset_of_forall_monomial {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (G : Manifold.HypersurfaceFamily X.carrier) (J : X.IdealSheaf) (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) : Manifold.IdealSheaf.support J ⊆ G.support

The support of a pointwise boundary monomial lies in the boundary: off the boundary the monomial is the empty product, the unit ideal.