Hironaka's normal crossings with a centre are Kollár's

The direction Hironaka's Definition 2 [Hir64, Definition 2, p. 141] → [Kol07, Definition 24 (4)] of the dictionary hasOnlyNormalCrossingsWith_idealSheaf_iff (the other direction is in Hironaka/Manifold/Snc/Dictionary.lean). At a point x of the closed submanifold Y, Definition 2 gives a regular system of parameters z_1, …, z_m of 𝒪_{M,x} such that every minimal prime of the stalk E_x of the reduced ideal sheaf of the snc divisor F is some (z_i) and the ideal (𝓘_Y)_x is generated by the z_i, i ∈ s. Then:

• the z_i are the coordinates of a chart e at x (the chart-extension theorem exists_chart_extending, as in Hironaka/Manifold/Snc/NonSingular.lean);
• (𝓘_Y)_x is also generated by the c adapted coordinates of a chart of Y at x; two families of parameters generating the same ideal have the same size (IsRegularLocalRing.card_eq_of_span_range_eq, the dimension count of [TSPA, Tag 00NQ] applied twice), so |s| = c; the identity (𝓘_Y)_y = (z_i)_{i∈s} spreads to a neighbourhood (exists_opens_stalkIdeal_eq_span), where Y = {z_i = 0, i ∈ s}, so e restricted there is adapted to Y with the block s;
• in the snc chart φ of F at x, E_x = (∏_{j : x ∈ E^j} w_j) with w_j the coordinate of the component E^j (Hironaka/Manifold/Snc/Coherence.lean); each (w_j) is a minimal prime of E_x (IsLocalRing.mem_minimalPrimes_span_prod), hence (w_j) = (z_{i_j}), i.e. w_j and z_{i_j} are associated; a unit germ is a nowhere-vanishing function near x, so E^j = {w_j = 0} = {z_{i_j} = 0} near x (exists_nhds_coord_eq_zero_iff_of_associated), and e is an snc chart of F at x with the indices i_j (injective, because distinct w_j are not associated).

With Hironaka/Manifold/Snc/Dictionary.lean this shows that, for the reduced ideal sheaf of an snc family, Hironaka's stalk-local normal crossings with a centre is exactly Kollár's simple normal crossings with it; the two readings of normal crossings differ only for boundaries that are not given by an snc family.

A unit germ is a nowhere-vanishing function near the point

theorem Manifold.exists_nhds_coord_eq_zero_iff_of_associated {𝕜 : 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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {x : M} (hx : x ∈ φ.source) (k : Fin n) {U : TopologicalSpace.Opens M} (hxU : x ∈ U) (g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) (hassoc : Associated (coord E ψ φ hφ hx k) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U x hxU)) g)) : ∃ (V : Set M), IsOpen V ∧ x ∈ V ∧ V ⊆ φ.source ∧ V ⊆ ↑U ∧ ∀ y ∈ V, ψ (↑φ y) k = 0 ↔ extendSection 𝕜 E g y = 0

If the coordinate z_k of a chart at x and the germ of a section g are associated in 𝒪_{M,x}, then near x the zero sets of z_k and of g coincide: the unit relating them is a function without zeros near x.

The converse dictionary

theorem Manifold.HypersurfaceFamily.exists_adaptedChart_isSncChartAt_of_parameters {𝕜 : 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} {Y : Set M} {c : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hF : IsSnc ψ F) (hY : IsClosedSubmanifold ψ Y c) {x : M} (hxY : x ∈ Y) {m : ℕ} (z : Fin m → ↑((structureSheaf 𝕜 E M).presheaf.stalk x)) (hspan : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk x)) (hdim : ↑m = ringKrullDim ↑((structureSheaf 𝕜 E M).presheaf.stalk x)) (hmin : ∀ P ∈ (F.idealSheaf.stalkIdeal x).minimalPrimes, ∃ (i : Fin m), P = Ideal.span {z i}) (s : Finset (Fin m)) (hD : hY.idealSheaf.stalkIdeal x = Ideal.span (z '' ↑s)) : ∃ (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n) (cidx : { j : F.ι // x ∈ F.hyp j } → Fin n), IsAdaptedChart ψ Y φ σ ∧ IsSncChartAt ψ F φ x cidx

Hironaka's Definition 2 → [Kol07, Definition 24 (4)]: at a point x of the closed submanifold Y, a regular system of parameters z of 𝒪_{M,x} whose members generate the minimal primes of (F.idealSheaf)_x and, for i ∈ s, the ideal (𝓘_Y)_x, yields a chart adapted to Y which is an snc chart of F at x.

theorem Manifold.hasOnlyNormalCrossingsWith_idealSheaf_iff {𝕜 : 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) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith F.idealSheaf hY.idealSheaf ↔ HypersurfaceFamily.HasSncWith ψ F Y c

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