The support of a simple normal crossings boundary is an snc divisor set

isSncDivisorSet_of_isSncBoundary: the support of a simple normal crossings boundary E of an analytic K-space X (ClosedSubspace.IsSncBoundary: Kollár's Definition 24 read on the stalks of a locally finite family of closed subspaces [Kol07, Definition 24]) is an snc divisor set in the sense of AnalyticSpace.IsSncDivisorSet — at every point a chart of X by the analytic space of an analytic manifold M (exists_manifold_of_isNonsingular, Hironaka/AnalyticSpace/Manifold/StratumIso.lean) on which the support is the support of an snc hypersurface family of M (HypersurfaceFamily.IsSnc). The two formulations of clause (3) of the resolution theorem, the divisor form of [Kol07, Theorem 45 (3)] and the chart form, thus agree.

The lemmas:

• IsSncBoundary.space_isNonsingular: the pointwise clause gives a regular system of parameters at every stalk, so X is non-singular;
• IsSncFamily.exists_countable_reindex: the members with nonempty support of a locally finite family on the σ-compact X are countable — the countable, linearly ordered index type that a HypersurfaceFamily (Hironaka/Manifold/Snc/Defs.lean) carries;
• IsSncFamily.comap_ofRestrict: an snc family restricted to an open subspace;
• exists_isSncChartAt_of_isSncFamily, isClosedSubmanifold_support_of_isSncFamily, exists_hypersurfaceFamily_isSnc_of_isSncFamily — the manifold side: an snc family of closed subspaces of Sp(M) (ClosedSubspace.IsSncFamily, Hironaka/AnalyticSpace/SncFamily.lean) has, at every point a : M, an snc chart (HypersurfaceFamily.IsSncChartAt) in the sense of [Kol07, Definition 24]: a chart of the maximal atlas on whose source every member through a is a coordinate hyperplane, distinct members having distinct coordinates; hence every member's support is a closed submanifold of codimension one, and the supports of a countable, linearly ordered family form an snc hypersurface family of M with the same support;
• isSncDivisorSet_of_isSncBoundary: the family behind E (isSncBoundary_iff_exists_isSncFamily_divisorOf), restricted to the stratum and carried to Sp(M) along the chart (isSncFamily_comap_of_isIso), re-indexed, read as an snc hypersurface family, with the support identity by set algebra through the chart.

The chart is built as in exists_adaptedChart_of_isRegularLocalRing_quotient (Hironaka/Manifold/Snc/NonSingular.lean), read on the regular system of parameters z of the pointwise clause: sections representing the z_i near a (exists_sections_of_germs, Hironaka/Manifold/Snc/Spreading.lean) vanish at a and have independent differentials (IsRegularLocalRing.linearIndependent_toCotangent_of_span_eq, linearIndependent_cotangentClass_of_residueField, hasIndependentDifferentialsAt_iff_linearIndependent_cotangentClass'), so they are the coordinates σ i of a chart e at a (exists_chart_extending, Hironaka/Manifold/AdaptedChart.lean); the stalk identity (H j)_a = (z_{c j}) of each of the finitely many members through a spreads to an open neighbourhood (exists_opens_stalkIdeal_eq_span); on the restriction of e to their intersection a point lies on the member iff the coordinate germ z_{c j} is not a unit there iff the coordinate σ (c j) vanishes at it (mem_maximalIdeal_iff_eval). The independence of the differentials is the Jacobian criterion Hironaka invokes at [Hir64, Ch. 0, §1, p. 121].

Used by Hironaka/Resolution/Analytic/Kol07Thm45/CoproductGluedFamily.lean and Hironaka/Resolution/Analytic/Kol07Thm45/Glue/OverFamilyPartner.lean.

theorem AnalyticSpace.ClosedSubspace.IsSncBoundary.space_isNonsingular {K : Type} [RCLike K] {X : AnalyticSpace K} {E : X.ClosedSubspace} (h : E.IsSncBoundary) : X.IsNonsingular

A space carrying an snc boundary is non-singular: the pointwise clause of IsSncBoundary gives a regular system of parameters at every stalk.

theorem AnalyticSpace.ClosedSubspace.IsSncFamily.exists_countable_reindex {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {H : ι → X.ClosedSubspace} (h : IsSncFamily H) : ∃ (ι' : Type u) (_ : Countable ι') (x : LinearOrder ι') (H' : ι' → X.ClosedSubspace), IsSncFamily H' ∧ ⋃ (j : ι'), Manifold.IdealSheaf.support (H' j) = ⋃ (j : ι), Manifold.IdealSheaf.support (H j)

An snc family on the σ-compact space X re-indexed by a countable linearly ordered type, the empty members dropped, with the same support.

theorem AnalyticSpace.ClosedSubspace.IsSncFamily.comap_ofRestrict {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {H : ι → X.ClosedSubspace} (h : IsSncFamily H) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : IsSncFamily fun (j : ι) => QuotientSpace.comap (↑(X.ofRestrict U)) (H j)

An snc family restricted to an open subspace: the pointwise clause is read back along the stalk isomorphisms KLocallyRingedSpace.isIso_ofRestrict_stalkMap.

theorem AnalyticSpace.exists_isSncChartAt_of_isSncFamily {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} {ι : Type u} {H : ι → (toSpace ψ M).ClosedSubspace} (h : ClosedSubspace.IsSncFamily H) (a : M.carrier) : ∃ (φ : OpenPartialHomeomorph M.carrier E) (cidx : { j : ι // a ∈ Manifold.IdealSheaf.support (H j) } → Fin n), φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M.carrier ∧ a ∈ φ.source ∧ Function.Injective cidx ∧ ∀ (j : { j : ι // a ∈ Manifold.IdealSheaf.support (H j) }), ∀ y ∈ φ.source, y ∈ Manifold.IdealSheaf.support (H ↑j) ↔ ψ (↑φ y) (cidx j) = 0

An snc chart at every point ([Kol07, Definition 24]): for an snc family of closed subspaces of Sp(M) and a point a : M, a chart of M at a on whose source every member through a is a coordinate hyperplane, distinct members having distinct coordinates — exists_chart_extending on the regular system of parameters at a, the stalk identities of the members through a spread by exists_opens_stalkIdeal_eq_span.

theorem AnalyticSpace.isClosedSubmanifold_support_of_isSncFamily {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} {ι : Type u} {H : ι → (toSpace ψ M).ClosedSubspace} (h : ClosedSubspace.IsSncFamily H) (j : ι) : Manifold.IsClosedSubmanifold ψ (Manifold.IdealSheaf.support (H j)) 1

Each member's support is a closed submanifold of codimension one ([Kol07, Definition 24]: each member is smooth): the snc chart at a point of the member, and isClosed_cosupport.

theorem AnalyticSpace.exists_hypersurfaceFamily_isSnc_of_isSncFamily {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} {ι : Type u} [Countable ι] [LinearOrder ι] {H : ι → (toSpace ψ M).ClosedSubspace} (h : ClosedSubspace.IsSncFamily H) : ∃ (F : Manifold.HypersurfaceFamily M.carrier), Manifold.HypersurfaceFamily.IsSnc ψ F ∧ F.support = ⋃ (j : ι), Manifold.IdealSheaf.support (H j)

The supports of a countable, linearly ordered snc family of closed subspaces of Sp(M) form an snc hypersurface family of M with the same support ([Kol07, Definition 24]).

theorem AnalyticSpace.ClosedSubspace.isSncDivisorSet_of_isSncBoundary {K : Type} [RCLike K] {X : AnalyticSpace K} (E : X.ClosedSubspace) (h : E.IsSncBoundary) : X.IsSncDivisorSet (Manifold.IdealSheaf.support E)

The support of an snc boundary is an snc divisor set: the chart of the stratum exists_manifold_of_isNonsingular, the family transported along it (isSncFamily_comap_of_isIso, support_comap_eq_preimage), exists_hypersurfaceFamily_isSnc_of_isSncFamily on the manifold, and the support identity from isSncBoundary_iff_exists_isSncFamily_divisorOf and support_divisorOf.