Simple normal crossings divisor sets: locality and density of the complement

AnalyticSpace.IsSncDivisorSet X Z, defined here: every point has an open neighbourhood U and a K-isomorphism e : Sp(M) ≅ X | U with the space of an analytic manifold carrying an snc hypersurface family F whose support e maps onto Z ∩ U. Clause (3) of the resolution theorem, [Kol07, Theorem 45 (3)], is checked in this form on the pieces of a gluing.

• isSncDivisorSet_of_openCover: the predicate is local on the space — a chart of the open subspace X | Vᵢ at a point is a chart of X there, through restrictOpen_restrictOpen_iso ((X | Vᵢ) | U' ≅ X | imageOpens, Hironaka/AnalyticSpace/OpenSubspaceLemmas.lean), the support equation read through Subtype.val;
• IsSncDivisorSet.dense_compl: the complement of an snc divisor set is dense — in each chart the complement of the support of an snc family is dense in the manifold (HypersurfaceFamily.IsSnc.dense_compl_support, Hironaka/Manifold/Snc/Dense.lean), transported along the homeomorphism underlying e. This gives the range clause of the resolution theorem its content (Hironaka/Resolution/Analytic/Kol07Thm45/ResolutionSnc.lean); compare [Hir64, Introduction] (the simple locus of a reduced complex space is dense) and [BM97, Remarks 1.7 (2)] (X.regularLocus Zariski-dense in a geometric space);
• val_toFun_restrictOpen_restrictOpen_iso_hom: the point of X under the restriction-of-restriction isomorphism.

Used by Hironaka/AnalyticSpace/SncBoundaryChart.lean and Hironaka/AnalyticSpace/SncDivisorSetCover.lean.

def AnalyticSpace.IsSncDivisorSet {K : Type} [RCLike K] (X : AnalyticSpace K) (Z : Set ↑↑X.toPresheafedSpace) : Prop

Z is the set of points of a simple normal crossings divisor of the non-singular space X ([Kol07, Theorem 45 (3)]; Hironaka's Definition 2 with D = X, [Hir64, Ch. 0, §5]): every point x has an open neighbourhood U and a K-isomorphism e : Sp(M) ≅ X | U with the space Sp(M) of an analytic manifold M modelled on K^d (AnalyticSpace.toSpace; on a non-singular space such charts exist) carrying a simple normal crossings hypersurface family F on M (HypersurfaceFamily.IsSnc) whose support e maps onto Z ∩ U. The coordinates on K^d are the identity.

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticSpace.val_toFun_restrictOpen_restrictOpen_iso_hom {K : Type} [RCLike K] {A : KLocallyRingedSpace K} (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(A.restrictOpen U).toPresheafedSpace) (w : ↑↑((A.restrictOpen U).restrictOpen V).toPresheafedSpace) : ↑(KLocallyRingedSpace.Hom.toFun (KLocallyRingedSpace.restrictOpen_restrictOpen_iso U V).hom w) = ↑↑w

The point of A under the restriction-of-restriction isomorphism (A|U)|V ≅ A|imageOpens U V is the point of A under the two inclusions.

theorem AnalyticSpace.isSncDivisorSet_of_openCover {K : Type} [RCLike K] (X : AnalyticSpace K) (Z : Set ↑↑X.toPresheafedSpace) {ι : Type u_1} (V : ι → Set ↑↑X.toPresheafedSpace) (hV : ∀ (i : ι), IsOpen (V i)) (hcov : ⋃ (i : ι), V i = Set.univ) (h : ∀ (i : ι), (X.restrictSet (V i)).IsSncDivisorSet (Subtype.val ⁻¹' Z)) : X.IsSncDivisorSet Z

The snc-divisor-set property is local on the space: it holds when it holds on the open subspaces of an open cover ([Kol07, Theorem 45 (3)], checked on the pieces of a gluing). At x ∈ Vᵢ, the chart e : Sp(M) ≅ (X | Vᵢ) | U' of the hypothesis composed with (X | Vᵢ) | U' ≅ X | imageOpens is a chart of X at x, and the support equation is read through Subtype.val.

theorem AnalyticSpace.IsSncDivisorSet.dense_compl {K : Type} [RCLike K] {X : AnalyticSpace K} {Z : Set ↑↑X.toPresheafedSpace} (hZ : X.IsSncDivisorSet Z) : Dense Zᶜ

The complement of an snc divisor set is dense (compare [Hir64, Introduction] and [BM97, Remarks 1.7 (2)]): at every point, the chart e : Sp(M) ≅ X | U carries the dense complement of the snc support (IsSnc.dense_compl_support) onto the complement of Z in X | U.