An snc support is Zariski-local

[Kol07, Definition 24] is a pointwise condition: a divisor E = ∑ E^i has simple normal crossings iff at every point x there are local coordinates z₁, …, zₙ with each component through x one of the coordinate hypersurfaces. Consequently, the EXISTENCE of an snc family with a given support S is a Zariski-local question: if every piece 𝒰.X i of an open cover of Y carries an snc family whose support is the preimage of S, then Y carries one with support S (exists_snc_of_openCover). The witness is the family of the irreducible components of S with their reduced structure (componentFamily of the vanishing ideal of S, Hironaka.Scheme.Snc.Dictionary): locally at x = 𝒰.f i w each component through x is the reduced component of a generic point η of S, η = 𝒰.f i η' with η' a generic point of the local support, hence of one member F^j of the local family (the members' supports cover the local support), so its stalk at x is the stalk of F^j at w transported along the stalk isomorphism of the open immersion — the coordinate z_{c(j)} of the local snc data (stalkIdeal_vanishingIdeal_closure_eq_of_isRegular_subscheme). The dictionary between the reduced components and the snc data (componentFamily_isSncAt_iff: snc at x iff every minimal prime of the stalk of S is a coordinate) then gives IsSncAt at x with the transported coordinates, and the members are regular because their stalk quotients are those of the local members (isRegular_subscheme_of_isRegularLocalRing_quotient). This is how clause (3) of [Kol07, Theorem 36] — Π⁻¹(Sing X) an snc divisor — is checked on the last stage of the resolution from its restrictions to an affine cover (Hironaka.Resolution.Algebraic.Kol07.Thm36.ClauseLocality).

Finiteness. The statement needs [NoetherianSpace Y] (so that S has finitely many irreducible components, Closeds.genericPoints_finite): without it the conclusion is FALSE — on the infinite disjoint union ⨆ₙ 𝔸² with S ∩ 𝔸²ₙ a configuration of n lines in general position, every piece carries an snc family (n members), but the members of any snc family are regular, so two crossing lines lie in different members and a global family would need infinitely many. The last stage of a blow-up sequence of a scheme of finite type over a field has a Noetherian space.

• Closeds.mem_genericPoints_of_le — a generic point of Z lying in a closed Z' ≤ Z is a generic point of Z';
• AlgebraicGeometry.Scheme.DivisorFamily.mem_support_iff_exists — a point lies in the support of a family iff on one of its members;
• isClosed_of_openCover — a set whose preimages under the pieces of an open cover are closed is closed;
• preimage_closure_singleton — the preimage of closure {ι η} along an open immersion ι is closure {η};
• exists_stalkIdeal_vanishingIdeal_closure_eq — the local identification of the stalk of a reduced component of S at ι w with the transported stalk of a member of the local family;
• exists_snc_of_openCover — the theorem.

Sources: [Kol07, Definition 24] (the pointwise condition); [Hir64, Definition 2] (normal crossings through a regular system of parameters, the form the dictionary uses).

theorem TopologicalSpace.Closeds.mem_genericPoints_of_le {α : Type u_1} [TopologicalSpace α] [T0Space α] [QuasiSober α] {Z Z' : Closeds α} (hle : Z' ≤ Z) {η : α} (hη : η ∈ Z.genericPoints) (hη' : η ∈ Z') : η ∈ Z'.genericPoints

A generic point of a closed set Z lying in a closed subset Z' ≤ Z is a generic point of Z' (Closeds.mem_genericPoints_iff: the closure of the point is a maximal irreducible subset of Z, hence of Z').

theorem Hironaka.Snc.isClosed_of_openCover {Y : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (S : Set ↥Y) (h : ∀ (i : 𝒰.I₀), IsClosed (⇑(𝒰.f i) ⁻¹' S)) : IsClosed S

A subset of Y whose preimages under the pieces of an open cover are closed is closed: its complement is the union of the images of the open preimages of the complement under the (open) pieces, which cover Y.

theorem Hironaka.Snc.preimage_closure_singleton {Y W : AlgebraicGeometry.Scheme} (ι : W ⟶ Y) [AlgebraicGeometry.IsOpenImmersion ι] (η : ↥W) : (TopologicalSpace.Closeds.closure {ι η}).preimage ⋯ = TopologicalSpace.Closeds.closure {η}

The preimage of the closure of a point along an open immersion is the closure of the point (an open embedding commutes with closures and is injective).

theorem Hironaka.Snc.exists_stalkIdeal_vanishingIdeal_closure_eq {Y W : AlgebraicGeometry.Scheme} (ι : W ⟶ Y) [AlgebraicGeometry.IsOpenImmersion ι] [TopologicalSpace.NoetherianSpace ↥Y] (S : TopologicalSpace.Closeds ↥Y) {F : W.DivisorFamily} (hF : F.IsSnc) (hsupp : ↑F.support = ⇑ι ⁻¹' ↑S) {η : ↥Y} (hη : η ∈ S.genericPoints) {w : ↥W} (hηw : η ⤳ ι w) : ∃ (j : F.ι), w ∈ (F.component j).support ∧ (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal (ι w) = Ideal.map (Sequence.stalkEquivOfIsOpenImmersion ι w).symm ((F.component j).stalkIdeal w)

The local identification behind exists_snc_of_openCover. Let S be closed in the Noetherian Y, ι : W ⟶ Y an open immersion, F an snc family on W with support ι⁻¹ S, η a generic point of S specializing to ι w. Then η = ι η' with η' a generic point of the support of some member F^j through w, and the stalk at ι w of the reduced component closure {η} is the stalk of F^j at w transported along the stalk isomorphism of ι (stalkIdeal_vanishingIdeal_closure_eq_of_isRegular_subscheme on W, the pull-back of a vanishing ideal along a smooth morphism comap_vanishingIdeal_of_smooth, and stalkIdeal_eq_map_symm_stalkIdeal_comap).

theorem Hironaka.Snc.exists_snc_of_openCover {Y : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥Y] (S : Set ↥Y) (𝒰 : Y.OpenCover) (h : ∀ (i : 𝒰.I₀), ∃ (F : (𝒰.X i).DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑(𝒰.f i) ⁻¹' S) : ∃ (F : Y.DivisorFamily), F.IsSnc ∧ ↑F.support = S

An snc support is Zariski-local ([Kol07, Definition 24] is pointwise). If every piece of an open cover of the Noetherian Y carries a simple normal crossing family whose support is the preimage of S, then Y carries one with support S — the family of the irreducible components of S with their reduced structure (componentFamily of the vanishing ideal of S): its support is S (support_componentFamily), at x = 𝒰.f i w its snc data are the local family's coordinates transported along the stalk isomorphism (componentFamily_isSncAt_iff, each minimal prime of the stalk of S being the stalk of a reduced component through x, exists_stalkIdeal_vanishingIdeal_closure_eq), and its members are regular because their stalk quotients are those of the local members. The hypothesis [NoetherianSpace Y] is the finiteness the statement needs (module docstring).