Simple normal crossings divisors and Hironaka's Definition 2

The dictionary between Kollár's simple normal crossings divisors (HypersurfaceFamily.IsSnc, HasSncWith, [Kol07, Definition 24]) and the stalk-level predicates of Hironaka's Definition 2 [Hir64, Definition 2, p. 141] (IdealSheaf.IsReduced, IdealSheaf.IsInvertible, IdealSheaf.HasOnlyNormalCrossingsWith) on the reduced ideal sheaf F.idealSheaf of the divisor, whose stalks Hironaka/Manifold/Snc/Coherence.lean computed: at a point x with snc chart φ and indices c, (F.idealSheaf)_x = (∏_{j : x ∈ E^j} z_{c j}), a product of distinct coordinates, each a prime element of the regular local ring 𝒪_{M,x}; the algebra of products of primes is Hironaka/Algebra/Local/PrimeProducts.lean.

• E reduced (Hironaka's "no nilpotent elements" [Hir64, p. 111]): a product of pairwise non-associated primes generates a radical ideal (a prime dividing a power divides the element).
• E invertible ("everywhere of codimension one" [Hir64, Definition 2, p. 141]): the product is a non-zero-divisor of the domain 𝒪_{M,x}.
• E has only normal crossings (Definition 2 with D = M): the centred coordinates z_i − z_i(x) of the snc chart are a regular system of parameters (𝔪_x = (z_i − z_i(x)), dim 𝒪_{M,x} = n), the minimal primes of (∏ z_{c j}) are the (z_{c j}) (a prime containing the product contains a factor, and (z_{c j}) is prime), and the ideal of D = M is ⊥ = (∅).
• Y has simple normal crossings with F implies Definition 2 for (E, D) = (F.idealSheaf, 𝓘_Y) ([Kol07, Definition 24 (4)] → [Hir64, Definition 2]; the converse is hasOnlyNormalCrossingsWith_idealSheaf_iff of Hironaka/Manifold/Snc/NormalCrossings.lean): at x ∈ Y the chart adapted to Y and snc for F gives the parameters; (𝓘_Y)_x = (z_{σ i}) is (z '' s) for s the image of σ.
• Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) is the reduced ideal sheaf of Kollár's total transform ([Hir64, Main Theorem II'(N) (iii), p. 156] and [Kol07, Definition 25] agree): both are the vanishing ideal sheaf of the closed set π⁻¹(|F|) ∪ π⁻¹(Y) = |Π⁻¹_tot(F)| (support_totalTransform), whose stalks have local generators because the total transform is snc — so the guarded branch of the definition of the reduced transform is taken.

These are the facts that identify the boundary clauses of the main theorems, stated through IsSncBoundary and IsSncBoundaryWith, with the boundary families the resolution algorithm carries (Hironaka/Manifold/FiniteSuccession/BoundaryFamily.lean).

The coordinates of the components through a point, at that point

theorem Manifold.HypersurfaceFamily.IsSncChartAt.coord_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] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a c) (j : { j : F.ι // a ∈ F.hyp j }) : ψ (↑φ a) (c j) = 0

The coordinates of the components through a vanish at a.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.prime_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a c) (j : { j : F.ι // a ∈ F.hyp j }) : Prime (coord E ψ φ ⋯ ⋯ (c j))

The coordinates of the components through a are prime elements of 𝒪_{M,a}.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.not_coord_dvd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a c) {i j : { j : F.ι // a ∈ F.hyp j }} (hij : i ≠ j) : ¬coord E ψ φ ⋯ ⋯ (c i) ∣ coord E ψ φ ⋯ ⋯ (c j)

The coordinates of two distinct components through a do not divide each other.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.span_range_centred_eq_and_dim {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a c) : Ideal.span (Set.range fun (i : Fin n) => coord E ψ φ ⋯ ⋯ i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ ⋯ ⋯ i))) = IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ∧ ↑n = ringKrullDim ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The centred coordinates z_i − z_i(a) of a chart: a regular system of parameters of 𝒪_{M,a} (they generate 𝔪_a, and dim 𝒪_{M,a} = n).

theorem Manifold.HypersurfaceFamily.centred_coord_eq_of_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] {φ : OpenPartialHomeomorph M E} {a : M} {hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M} {ha : a ∈ φ.source} {k : Fin n} (h0 : ψ (↑φ a) k = 0) : coord E ψ φ hφ ha k - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha k)) = coord E ψ φ hφ ha k

For a coordinate vanishing at a, the centred coordinate is the coordinate itself.

theorem Manifold.HypersurfaceFamily.IsSnc.isRadical_stalkIdeal_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (x : M) : (F.idealSheaf.stalkIdeal x).IsRadical

Hironaka's "E reduced" [Hir64, p. 111]: the stalks of the reduced ideal sheaf of an snc divisor are radical ideals.

theorem Manifold.HypersurfaceFamily.IsSnc.exists_nonZeroDivisor_stalkIdeal_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (x : M) : ∃ g ∈ nonZeroDivisors ↑((structureSheaf 𝕜 E M).presheaf.stalk x), F.idealSheaf.stalkIdeal x = Ideal.span {g}

Hironaka's "everywhere of codimension one" [Hir64, Definition 2, p. 141]: the stalks of the reduced ideal sheaf of an snc divisor are generated by a single non-zero-divisor.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.minimalPrimes_stalkIdeal_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hF : IsSnc ψ F) (hc : IsSncChartAt ψ F φ a c) {P : Ideal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)} (hP : P ∈ (F.idealSheaf.stalkIdeal a).minimalPrimes) : ∃ (i : Fin n), P = Ideal.span {coord E ψ φ ⋯ ⋯ i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ ⋯ ⋯ i))}

The minimal primes of Hironaka's Definition 2: in an snc chart at x, the minimal primes of the stalk of the reduced ideal sheaf are the ideals of the coordinates of the components through x, read in the centred coordinates of the chart.

The predicates of Definition 2 on bundled manifolds

theorem Manifold.isReduced_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily N.carrier} (hF : HypersurfaceFamily.IsSnc ψ F) : AnalyticManifold.IdealSheaf.IsReduced F.idealSheaf

The reduced ideal sheaf of an snc divisor is reduced ([Hir64, Definition 2, p. 141], "E reduced").

theorem Manifold.isInvertible_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily N.carrier} (hF : HypersurfaceFamily.IsSnc ψ F) : F.idealSheaf.IsInvertible

The reduced ideal sheaf of an snc divisor is invertible ([Hir64, Definition 2, p. 141], "the sheaf of ideals of E is invertible").

theorem Manifold.hasOnlyNormalCrossings_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily N.carrier} (hF : HypersurfaceFamily.IsSnc ψ F) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossings F.idealSheaf

The reduced ideal sheaf of an snc divisor has only normal crossings in Hironaka's sense ([Hir64, Definition 2, p. 141] with D = M).

theorem Manifold.HasSncWith.hasOnlyNormalCrossingsWith_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily N.carrier} (hF : HypersurfaceFamily.IsSnc ψ F) {Y : Set N.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hsnc : HypersurfaceFamily.HasSncWith ψ F Y c) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith F.idealSheaf hY.idealSheaf

[Kol07, Definition 24 (4)] → [Hir64, Definition 2, p. 141]: if the closed submanifold Y has simple normal crossings with the snc divisor F, the reduced ideal sheaf of F has only normal crossings with the ideal sheaf of Y in Hironaka's sense.

theorem Manifold.reducedTransform_eq_idealSheaf_totalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N N' : AnalyticManifold 𝕜 E} {π : N'.carrier → N.carrier} {Y : Set N.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {F : HypersurfaceFamily N.carrier} (hF : HypersurfaceFamily.IsSnc ψ F) (hsnc : HypersurfaceFamily.HasSncWith ψ F Y c) : AnalyticManifold.IdealSheaf.reducedTransform ⟨π, ⋯⟩ F.idealSheaf hY.idealSheaf = (HypersurfaceFamily.totalTransform π Y F).idealSheaf

Hironaka's E_{λ+1} = red(f⁻¹(E_λ) ∪ f⁻¹(D_λ)) [Hir64, Main Theorem II'(N) (iii), p. 156] is Kollár's total transform [Kol07, Definition 25]: under the blowing-up of N along Y, the reduced transform of the reduced ideal sheaf of an snc divisor F having snc with Y is the reduced ideal sheaf of the snc total transform.