Simple-normal-crossings divisor sets on a glued space

On a gluing datum G : GlueOver X R π dom the pieces are the open immersions ιGlued i : R i → gluedOver, so the local predicate IsSncDivisorSet of the analytic-space vocabulary is checked piece by piece (isSncDivisorSet_of_openImmersion_cover, Hironaka.AnalyticSpace.SncDivisorSetCover); for the inverse image under the descended map of a subset of X the pieces' conditions are on the inverse images under the piece maps (toFun_descMap_ιGlued). This is how the clause that the inverse image of the singular locus is a divisor with simple normal crossings ([Kol07, Theorem 45, (3)]; [Wlo09, Theorem 2.0.1, (2)]) passes from the local resolutions to the glued space: isSncDivisorSet_gluedOver_preimage is applied twice in Hironaka.Resolution.Analytic.Kol07Thm45.ResolutionSnc, on each glued space of local resolutions and on the space glued along the exhaustion. The plain form isSncDivisorSet_gluedOver has no code users outside this module.

theorem AnalyticSpace.GlueOver.isSncDivisorSet_gluedOver {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (Z : Set ↑↑G.gluedOver.toPresheafedSpace) (h : ∀ (i : ι), (R i).IsSncDivisorSet (KLocallyRingedSpace.Hom.toFun (G.ιGlued i) ⁻¹' Z)) : G.gluedOver.IsSncDivisorSet Z

A subset of a glued space is a simple-normal-crossings divisor set when its inverse image in every piece is: the pieces ιGlued i are open immersions covering the glued space (exists_ιGlued_eq).

theorem AnalyticSpace.GlueOver.isSncDivisorSet_gluedOver_preimage {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (S : Set ↑↑X.toPresheafedSpace) (h : ∀ (i : ι), (R i).IsSncDivisorSet (KLocallyRingedSpace.Hom.toFun (π i) ⁻¹' S)) : G.gluedOver.IsSncDivisorSet (KLocallyRingedSpace.Hom.toFun G.descMap ⁻¹' S)

The inverse image under the descended map of a subset S ⊆ X is a simple-normal-crossings divisor set of the glued space when its inverse image under every piece map is (toFun_descMap_ιGlued).