The exceptional members of the coproduct run: normal crossings and support

Two facts about the datum's exceptional members D.sigmaMembers bed W hW hbed (CoproductExceptionalFamily.lean): they form a simple normal crossings family of closed subspaces of the coproduct's local resolution Sp(Y_r) (ClosedSubspace.IsSncFamily), and the union of their supports is Π_Σ⁻¹(Y_Σ.singularLocus) — at the coproduct triple D.sigmaTriple over D.ambImage W, the counterparts of the per-piece facts of Hironaka/Resolution/Analytic/Wlo09/PreimageSing.lean ([Wlo09, Theorem 2.0.1(2)]; [Kol07, Definition 24]). The pieces of a datum are resolved by the ONE run on their disjoint union, so the facts are the per-piece proofs with the piece's triple replaced by an arbitrary admissible one — no new mathematics beyond one bridge.

The support. PieceEmbedding.localResolutionMap_preimage_sing_eq (Hironaka/Resolution/Analytic/Wlo09/PreimageSing.lean) is restated at an arbitrary admissible (T, W) (BEDanFamStar.localResolutionMapOn_preimage_sing_eq); its proof is the per-piece proof verbatim — hbed's clauses at (T, W) and the generic succession lemmas. The support of each traced member is the preimage of the member (QuotientSpace.cosupport_comap, support_toClosedSubspaces_apply) and |E_r| = ⋃ⱼ E_j by definition.

The simple normal crossings family. The trace bridge isSncFamily_comap_toAnalyticSpaceι_toClosedSubspaces (Kollár's definition of simple normal crossings with a subvariety, [Kol07, Definition 24], read on the members — the argument of isSncDivisorSet_toAnalyticSpace_of_forall at the level of the family): on an analytic manifold A, an ideal sheaf J with regular quotient stalks along its support and a simple normal crossings family F with a PROPER ADAPTED chart at every point of V(J) — an adapted chart of V(J) which is a simple normal crossings chart of F with the components' coordinates off V(J)'s block, the data IsProperSnc of Hironaka/Resolution/Analytic/Wlo09/ProperSnc.lean — trace to a simple normal crossings family of closed subspaces of V(J). At a point y of V(J) with image a the centred coordinates z_1, …, z_n of the chart are a regular system of parameters of 𝒪_{A,a}, J_a = (z_σ) (the vanishing ideal of V(J), by the local Hadamard lemma), and the stalk map of the closed immersion V(J) → A at y is the quotient map 𝒪_{A,a} → 𝒪_{A,a}/J_a: the images of the complementary coordinates generate 𝔪_y, they are n − c in number with dim 𝒪_{V(J),y} = n − c (the parameter count of the regular quotient, [TSPA, Tag 00NQ]), and the traced member j through y is cut out by the image of its coordinate z_{cidx j}, complementary by properness — the three clauses of IsSncFamily. The datum's run satisfies the hypotheses by hbed's clauses at the last stage (hbed.isProperSnc, Hironaka/Resolution/Analytic/Wlo09/ProperSncOfEmbeddedDesing.lean; clause (3) non-singularity through mem_reg_toAnalyticSpace_iff).

Not in the sources beyond Kollár's definition; bookkeeping.

The support identity at any admissible (T, W)

theorem Hironaka.Manifold.BEDanFamStar.localResolutionMapOn_preimage_sing_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) : ↑(bed.localResolutionMapOn T hT W hW) ⁻¹' (restrictedIdealOn T W).toAnalyticSpace.singularLocus = (fun (y : ↑↑(bed.lastIdealOn T hT W hW).toAnalyticSpace.toPresheafedSpace) => ↑(bed.lastIdealOn T hT W hW).toAnalyticSpaceι y) ⁻¹' ((bed.seqOn T hT W hW).toSuccession.totalTransformSeq (Fin.last (bed.seqOn T hT W hW).toSuccession.length)).support

Π⁻¹((Sp(W)/T.I|W).singularLocus) = Ỹ ∩ |E_r| for the functor's run on T|W ([Wlo09, Theorem 2.0.1(2)]) — localResolutionMap_preimage_sing_eq with the piece's triple replaced by an arbitrary admissible one; its proof transfers verbatim (hbed's clauses at (T, W): the centres over the non-simple points, the non-singularity of Ỹ; the generic succession lemmas).

The trace bridge: an snc family with a proper adapted snc chart at every point of the

smooth closed subspace V(J) traces to an snc family of closed subspaces of V(J)

theorem Hironaka.Manifold.isSncFamily_comap_toAnalyticSpaceι_toClosedSubspaces {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : A.IdealSheaf) (hns : ∀ a ∈ Manifold.IdealSheaf.support J, IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) A.carrier).presheaf.stalk a) ⧸ Manifold.IdealSheaf.stalkIdeal J a)) {F : Manifold.HypersurfaceFamily A.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F) (hproper : ∀ x ∈ Manifold.IdealSheaf.support J, ∃ (c : ℕ) (φ : OpenPartialHomeomorph A.carrier (Fin n → 𝕜)) (σ : Fin c ↪ Fin n) (cidx : { j : F.ι // x ∈ F.hyp j } → Fin n), Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.IdealSheaf.support J) φ σ ∧ Manifold.HypersurfaceFamily.IsSncChartAt (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F φ x cidx ∧ ∀ (j : { j : F.ι // x ∈ F.hyp j }), cidx j ∉ Set.range ⇑σ) : AnalyticSpace.ClosedSubspace.IsSncFamily fun (j : F.ι) => (F.toClosedSubspaces ⋯ j).comap J.toAnalyticSpaceι

The trace bridge ([Kol07, Definition 24], read on the members): at a point y of V(J) with image a, the proper adapted snc chart gives the centred coordinates z_1, …, z_n as a regular system of parameters of 𝒪_{A,a} with J_a = (z_σ); the stalk map of the closed immersion is the quotient map 𝒪_{A,a} → 𝒪_{A,a}/J_a, so the images of the complementary coordinates are a regular system of parameters of 𝒪_{V(J),y} (dimension n − c by the parameter count of the regular quotient), and the traced member j through y is cut out by the image of its coordinate z_{cidx j}, which is complementary by properness.

The two facts on the datum's single run

theorem Hironaka.Manifold.LocalEmbeddingData.isSncFamily_sigmaMembers {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : AnalyticSpace.ClosedSubspace.IsSncFamily (D.sigmaMembers bed W hW hbed)

The exceptional members of the datum's single run form a simple normal crossings family of closed subspaces of the coproduct's local resolution ([Kol07, Definition 24]) — the trace bridge at hbed's clauses on the coproduct run: Ỹ_Σ non-singular (clause (3)), E_r with simple normal crossings (clause (1)), a proper adapted chart at every point of Ỹ_Σ (hbed.isProperSnc).

theorem Hironaka.Manifold.LocalEmbeddingData.iUnion_support_sigmaMembers {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : ⋃ (j : D.sigmaIndex bed W hW), Manifold.IdealSheaf.support (D.sigmaMembers bed W hW hbed j) = ↑(bed.localResolutionMapOn D.sigmaTriple ⋯ (D.ambImage W) ⋯) ⁻¹' (BEDanFamStar.restrictedIdealOn D.sigmaTriple (D.ambImage W)).toAnalyticSpace.singularLocus

The union of the supports of the exceptional members is Π_Σ⁻¹(Y_Σ.singularLocus) ([Wlo09, Theorem 2.0.1(2)]) — localResolutionMapOn_preimage_sing_eq at the coproduct triple, and the support of each traced member is the preimage of the member.