Simple normal crossings families of a manifold as families of closed subspaces of Sp(M)

The members of a simple normal crossings family F of hypersurfaces of an analytic manifold M (HypersurfaceFamily.IsSnc, Hironaka/Manifold/Snc/Defs.lean), read as closed subspaces of the analytic space Sp(M) through their ideal sheaves (HypersurfaceFamily.toClosedSubspaces, Hironaka/AnalyticSpace/SncFamily.lean), form a simple normal crossings family of closed subspaces (ClosedSubspace.IsSncFamily) with the same support, so their divisor is an snc boundary of Sp(M) with support |F| — the form in which each piece of a glued resolution contributes its exceptional divisor ([Kol07, Theorem 45 (3)] on a piece).

• support_toClosedSubspaces_apply, support_toClosedSubspaces: the supports;
• isSncFamily_toClosedSubspaces: in an snc chart at a the centred coordinates are a regular system of parameters of the analytic stalk (maximalIdeal_eq_span_coord', Hironaka/Manifold/Germ/TaylorIdeal.lean; ringKrullDim_stalk_of_chart, Hironaka/Manifold/Germ/StalkNoetherian.lean) and each member through a is cut out by its coordinate (IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_span, Hironaka/Manifold/BlowUp/Transform/Object.lean);
• exists_isSncBoundary_toSpace_of_isSnc: the divisor of the members is an snc boundary of Sp(M) with support |F|.

Used by Hironaka/Resolution/Analytic/Kol07Thm45/CoproductExceptionalSnc.lean.

theorem Manifold.HypersurfaceFamily.support_toClosedSubspaces_apply {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} (F : HypersurfaceFamily M.carrier) (h : ∀ (j : F.ι), IsClosedSubmanifold ψ (F.hyp j) 1) (j : F.ι) : IdealSheaf.support (F.toClosedSubspaces h j) = F.hyp j

The support of a member read as a closed subspace of Sp(M) is the member (IsClosedSubmanifold.cosupport_idealSheaf); support_toClosedSubspaces is the union form.

theorem Manifold.HypersurfaceFamily.support_toClosedSubspaces {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} (F : HypersurfaceFamily M.carrier) (h : ∀ (j : F.ι), IsClosedSubmanifold ψ (F.hyp j) 1) : ⋃ (j : F.ι), IdealSheaf.support (F.toClosedSubspaces h j) = F.support

theorem Manifold.HypersurfaceFamily.isSncFamily_toClosedSubspaces {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ F) : AnalyticSpace.ClosedSubspace.IsSncFamily (F.toClosedSubspaces ⋯)

An snc family of hypersurfaces of M is an snc family of closed subspaces of Sp(M) ([Kol07, Definition 24]): in an snc chart at a the centred coordinates are a regular system of parameters of the analytic stalk (maximalIdeal_eq_span_coord', ringKrullDim_stalk_of_chart) and each member through a is cut out by its coordinate (IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_span).

theorem Manifold.HypersurfaceFamily.exists_isSncBoundary_toSpace_of_isSnc {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ F) : ∃ (E_1 : (AnalyticSpace.toSpace ψ M).ClosedSubspace), E_1.IsSncBoundary ∧ IdealSheaf.support E_1 = F.support

The divisor of the members of an snc family of hypersurfaces of M is an snc boundary of Sp(M) with support |F| ([Kol07, Theorem 45 (3)] on one piece of a glued resolution).