The snc-divisor predicate: restriction to open subspaces and locality on open-immersion covers

AnalyticSpace.IsSncDivisorSet X Z (at every point a chart Sp(M) ≅ X | U carrying an snc hypersurface family onto Z ∩ U) is a local predicate. Two consequences, needed to read clause (3) of the resolution theorem — the inverse image of the singular locus is an snc divisor set, [Kol07, Theorem 45 (3)] — off the pieces of a gluing:

• IsSncDivisorSet.restrictOpen: an snc divisor set restricts to every open subspace X | V — the chart at a point of V shrinks to the open submanifold M | W, W the trace of V, the family pulls back along the inclusion (isSnc_comap, a local diffeomorphism), and the shrunk chart is isoOfRangeEq of the composite open immersion Sp(M | W) → Sp(M) → X, with image in V;
• isSncDivisorSet_of_openImmersion_cover: Z is an snc divisor set when its inverse image in every piece of a cover by open immersions is — the open-immersion form of isSncDivisorSet_of_openCover (Hironaka/AnalyticSpace/SncDivisorSetLocal.lean).

Not in the sources: the predicate is the chart form of Hironaka's normal crossings [Hir64, Ch. 0, §5, Definition 2] and of [Kol07, Definition 24]. Used by Hironaka/AnalyticSpace/Glue/OverSnc.lean.

theorem AnalyticSpace.IsSncDivisorSet.restrictOpen {K : Type} [RCLike K] {X : AnalyticSpace K} {Z : Set ↑↑X.toPresheafedSpace} (hZ : X.IsSncDivisorSet Z) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : (X.restrictOpen V).IsSncDivisorSet (Subtype.val ⁻¹' Z)

An snc divisor set restricts to every open subspace: at x ∈ V the chart Sp(M) ≅ X | U of Z shrinks to the open submanifold M | W, W the points of M carried into V; the composite Sp(M | W) → Sp(M) → X | U → X is an open immersion with image in V, so isoOfRangeEq identifies Sp(M | W) with (X | V) | U', U' its image; the family F.comap (M.inclusion W) is snc (isSnc_comap along the local diffeomorphism isLocalDiffeomorph_inclusion) with support the trace of |F| (support_comap).

theorem AnalyticSpace.isSncDivisorSet_of_openImmersion_cover {K : Type} [RCLike K] (X : AnalyticSpace K) (Z : Set ↑↑X.toPresheafedSpace) {ι : Type u_1} (A : ι → AnalyticSpace K) (g : (i : ι) → (A i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) [hg : ∀ (i : ι), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(g i)] (hcov : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (i : ι) (a : ↑↑(A i).toPresheafedSpace), KLocallyRingedSpace.Hom.toFun (g i) a = x) (h : ∀ (i : ι), (A i).IsSncDivisorSet (KLocallyRingedSpace.Hom.toFun (g i) ⁻¹' Z)) : X.IsSncDivisorSet Z

The snc-divisor predicate is local on the target of a cover by open immersions: Z is an snc divisor set of X when its inverse image in every piece A i is — at x = g i a the chart Sp(M) ≅ (A i) | U' at a, composed with the identification of (A i) | U' with its image open in X (isoOfRangeEq of ofRestrict ≫ g i), is a chart of X at x, and the support equation is read through g i. The open-immersion form of isSncDivisorSet_of_openCover (Hironaka/AnalyticSpace/SncDivisorSetLocal.lean).