The divisor of a simple normal crossings family: support and boundary predicate

For ClosedSubspace.divisorOf and ClosedSubspace.IsSncFamily of Hironaka/AnalyticSpace/SncFamily.lean:

• support_divisorOf: the support of the divisor of a locally finite family is the union of the members' supports;
• isSncBoundary_divisorOf: the divisor of an snc family is an snc boundary (ClosedSubspace.IsSncBoundary), Kollár's E = Σ Eᵢ with simple normal crossings [Kol07, Definition 24] (the boundary of [Kol07, Theorem 45 (3)] and [Wlo09, Theorem 2.0.1 (2)]);
• isSncBoundary_iff_exists_isSncFamily_divisorOf: conversely every snc boundary is the divisor of an snc family, so IsSncBoundary is exactly "the divisor of an snc family";
• isSncBoundary_top_iff_isNonsingular: the boundary case — the empty divisor ⊤ is an snc boundary iff X is non-singular.

Used by Hironaka/Resolution/Analytic/Kol07Thm45/ResolutionSncGlobal.lean, Hironaka/AnalyticSpace/SncFamilyManifold.lean and Hironaka/AnalyticSpace/SncBoundaryChart.lean.

theorem AnalyticSpace.ClosedSubspace.support_divisorOf {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} (H : ι → X.ClosedSubspace) (hH : LocallyFinite fun (j : ι) => Manifold.IdealSheaf.support (H j)) : Manifold.IdealSheaf.support (divisorOf H hH) = ⋃ (j : ι), Manifold.IdealSheaf.support (H j)

The support of the divisor of a locally finite family is the union of the members' supports (Kollár's E = Σ Eᵢ, [Kol07, Definition 24]): a finite product of proper ideals of a local ring is proper, and off every member the product is the unit ideal.

theorem AnalyticSpace.ClosedSubspace.isSncBoundary_divisorOf {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {H : ι → X.ClosedSubspace} (h : IsSncFamily H) : (divisorOf H ⋯).IsSncBoundary

The divisor of an snc family is an snc boundary ([Kol07, Definition 24]): the body of IsSncBoundaryWith read off stalkIdeal_divisorOf with the finset s := Finset.univ.image c on the finite subtype of the members through x.

theorem AnalyticSpace.ClosedSubspace.isSncBoundary_iff_exists_isSncFamily_divisorOf {K : Type} [RCLike K] {X : AnalyticSpace K} (E : X.ClosedSubspace) : E.IsSncBoundary ↔ ∃ (ι : Type u) (H : ι → X.ClosedSubspace) (hH : LocallyFinite fun (j : ι) => Manifold.IdealSheaf.support (H j)), IsSncFamily H ∧ E = divisorOf H hH

IsSncBoundary is exactly "the divisor of an snc family".

theorem AnalyticSpace.ClosedSubspace.isSncBoundary_top_iff_isNonsingular {K : Type} [RCLike K] {X : AnalyticSpace K} : ⊤.IsSncBoundary ↔ X.IsNonsingular

The boundary case: the empty divisor ⊤ (the unit ideal) is an snc boundary iff every stalk of X is a regular local ring, i.e. iff X is non-singular — IsSncBoundary presupposes a regular system of parameters at every point (Mathlib's IsRegularLocalRing.of_spanFinrank_maximalIdeal_le, IsLocalRing.exists_regularSystem; the analytic stalks are Noetherian, isNoetherianRing_stalk).