Włodarczyk's embedded desingularization on the standard model

The analytic embedded desingularization of a reduced closed subspace Y of an analytic manifold M modelled on the standard space 𝕜ⁿ [Wlo09, Theorem 2.0.2], as one extension-compatible family over M, with its clauses per compact and its commutation with local analytic isomorphisms. The main theorem AnalyticManifold.exists_embeddedDesingularization is in Hironaka/Resolution/Analytic/Wlo09/EmbeddedDesingularization.lean; the global objects on the glued space, in Hironaka/Resolution/Analytic/Wlo09/EmbeddedDesingGlobal.lean.

For an ideal sheaf with nonzero stalks, the family is the concrete embedded desingularization functor concreteBEDanFamStar (Hironaka/Resolution/Analytic/Wlo09/Concrete.lean) at the triple (M, 𝓘_Y, ∅) (embeddedTriple), a compatible family of successions over the relatively compact opens (embeddedDesingPiecesOfNonzero), glued along the exhaustion of M (CompatibleFamily.toExtensionCompatibleFamily, the gluing of resolveFamExt, Hironaka/Resolution/Analytic/Wlo09/FamilyExt.lean; embeddedDesingFamOfNonzero):

• isProperMap_embeddedDesingFamOfNonzero_map: the glued blow-down is proper (CompatibleFamily.isProperMap_limitBlowDown);
• isAnalyticIsoOver_embeddedDesingFamOfNonzero_map: it is an isomorphism off the singular locus Sing(Y) = Y ∖ Reg(Y): the centres lie over Y (the order clause of the modified marked resolution, bedanFamOfInput_isOfOrderGe, read by CentersOver.of_isOfOrderGe) and avoid Reg(Y) (clause (2) of IsEmbeddedDesing), so every blow-down of a piece is an isomorphism over the complement of Sing(Y) (isAnalyticIsoOver_stageMap), and these glue (CompatibleFamily.isAnalyticIsoOver_limitBlowDown);
• isDesingularizedBy_seqOn_embeddedDesingPiecesOfNonzero: over every relatively compact open the succession desingularizes the restriction of Y (IdealSheaf.IsDesingularizedBy). Clauses (1), (2), (3) and (6) are those of concreteBEDanFamStar_isEmbeddedDesing, (1) read in Hironaka's boundary form (hasOnlyNormalCrossingsWith_boundarySeq_of_forall_hasSncWith, boundarySeq_eq_idealSheaf_totalTransformSeq_of_forall_lt; boundarySeq_seqOn_embeddedDesingPiecesOfNonzero), (3) in its transversal form (IsEmbeddedDesing.isProperSnc); the support of the last exceptional divisor is the preimage of Sing(Y): it lies over the centres, hence over Sing(Y) (support_totalTransformSeq_subset_preimage_of_centersOver), and off it the composite blow-down is an isomorphism near the point, carrying the smooth strict transform onto Y (isRegularLocalRing_quotient_strictTransformSubspaceSeq_iff_of_notMem_support).

For an arbitrary reduced 𝓘_Y, which may vanish on some connected components of M (those contained in Y), the family embeddedDesingFam is the one of 𝓘_Y made the unit ideal on those components (IdealSheaf.unitOnZeroStalks, Hironaka/Resolution/Analytic/Wlo09/ZeroStalks.lean; the pieces embeddedDesingPieces), whose singular locus is that of Y; over the components where 𝓘_Y vanishes nothing is blown up, and the clauses transfer (IsDesingularizedBy.of_eq_off_clopen, isDesingularizedBy_seqOn_embeddedDesingPieces): there the strict transform is the component itself, smooth, and the exceptional divisor is empty. The transversal chart clause (3) and the monomial clause (6) are also recorded with the last exceptional family named explicitly (exists_adaptedChart_seqOn_embeddedDesingPieces, exists_monomial_seqOn_embeddedDesingPieces), the form in which the global objects are glued.

The family commutes with local analytic isomorphisms over every pair of compacts (isPullbackUpToEmptyAlong_embeddedDesingFam): for a local analytic isomorphism g : N → M and J = g^*I, the triple of J carries the pull-back data of the triple of I (making the unit ideal on the zero components commutes with the pull-back, unitOnZeroStalks_pullback_of_isLocalDiffeomorph), so the values of the functor correspond (CommutesWithLocalIsos, the last clause of IsEmbeddedDesing) and the succession over a compact of N is the pull-back up to empty blow-ups of the succession over every compact of M whose neighbourhood contains its image (CompatibleFamily.isPullbackUpToEmptyAlong_seqOn).

The triple of a closed subspace

def Hironaka.Manifold.embeddedTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M

The triple (M, 𝓘_Y, ∅) of the ideal sheaf 𝓘_Y of a closed subspace with nonzero stalks and the empty boundary, the input of the embedded desingularization functor.

Equations

• Hironaka.Manifold.embeddedTriple I hI₀ = { I := I, isNonzeroEverywhere := hI₀, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ }

theorem Hironaka.Manifold.domBEDan_embeddedTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) : DomBEDan 𝕜 (embeddedTriple I hI₀)

The triple (M, 𝓘_Y, ∅) of a reduced Y is in the class DomBEDan of the embedded desingularization functor.

The family of an ideal sheaf with nonzero stalks

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.embeddedDesingPiecesOfNonzero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) : CompatibleFamily (embeddedTriple I hI₀)

The pieces of the embedded desingularization of Y, for an ideal sheaf 𝓘_Y with nonzero stalks: the value of the concrete embedded desingularization functor concreteBEDanFamStar at (M, 𝓘_Y, ∅), a compatible family of successions over the relatively compact opens of M.

Equations

• Hironaka.Manifold.embeddedDesingPiecesOfNonzero M I hI hI₀ = ((Hironaka.concreteBEDanFamStar 𝕜).fam n).fam (Hironaka.Manifold.embeddedTriple I hI₀) ⋯

noncomputable def Hironaka.Manifold.embeddedDesingFamOfNonzero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) : M.ExtensionCompatibleFamily

The embedded desingularization of Y as one family over M, for an ideal sheaf 𝓘_Y with nonzero stalks: the pieces glued along the exhaustion of M ([Wlo09, Theorem 2.0.2]; the gluing of [Wlo09, §4.2]).

Equations

• Hironaka.Manifold.embeddedDesingFamOfNonzero M I hI hI₀ = (Hironaka.Manifold.embeddedDesingPiecesOfNonzero M I hI hI₀).toExtensionCompatibleFamily

theorem Hironaka.Manifold.isProperMap_embeddedDesingFamOfNonzero_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) : IsProperMap ⇑(embeddedDesingFamOfNonzero M I hI hI₀).map

The blow-down of the embedded desingularization is proper.

theorem Hironaka.Manifold.centersOver_embeddedTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.CentersOver (Manifold.IdealSheaf.support (I.restrict U) \ (I.restrict U).regularLocus)

The centres of the succession on a relatively compact open lie over Sing(Y) = Y ∖ Reg(Y) of Y ∩ U: over Y by the order clause of the modified marked resolution (bedanFamOfInput_isOfOrderGe, CentersOver.of_isOfOrderGe at mark 1), and off Reg(Y) by clause (2) of IsEmbeddedDesing.

theorem Hironaka.Manifold.isAnalyticIsoOver_embeddedDesingFamOfNonzero_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) : (embeddedDesingFamOfNonzero M I hI hI₀).map.IsIsoOver (Manifold.IdealSheaf.support I \ I.regularLocus)ᶜ

The blow-down of the embedded desingularization is an isomorphism off Sing(Y), Włodarczyk's bimeromorphy: every blow-down of a piece is an isomorphism over the complement of Sing(Y), the centres lying over it (centersOver_embeddedTriple, isAnalyticIsoOver_stageMap), and these glue (CompatibleFamily.isAnalyticIsoOver_limitBlowDown).

theorem Hironaka.Manifold.boundarySeq_top_eq_idealSheaf_totalTransformSeq_of_forall_hasSncWith {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (S : M'.FiniteSuccession) (h1b : ∀ (i : Fin S.length), Manifold.HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (S.totalTransformSeq i.castSucc) (Manifold.IdealSheaf.support (S.center i)) (S.codim i)) (i : Fin (S.length + 1)) : S.boundarySeq ⊤ i = (S.totalTransformSeq i).idealSheaf

The exceptional divisors of a succession whose centres have simple normal crossings with the exceptional families are the reduced ideal sheaves of those families: every boundary started at the empty boundary is the reduced ideal sheaf of the total transform of the empty family at that stage (the chart form read in Hironaka's boundary form by hasOnlyNormalCrossingsWith_boundarySeq_of_forall_hasSncWith and boundarySeq_eq_idealSheaf_totalTransformSeq_of_forall_lt).

theorem Hironaka.Manifold.boundarySeq_seqOn_embeddedDesingPiecesOfNonzero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin (((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.length + 1)) : ((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.boundarySeq ⊤ i = (((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.totalTransformSeq i).idealSheaf

The exceptional divisors are the reduced ideal sheaves of the exceptional families: on every relatively compact open, every boundary started at the empty boundary is the reduced ideal sheaf of the total transform of the empty family at that stage, since every centre has simple normal crossings with the exceptional family in the chart form (clause (1) of concreteBEDanFamStar_isEmbeddedDesing; boundarySeq_top_eq_idealSheaf_totalTransformSeq_of_forall_hasSncWith).

theorem Hironaka.Manifold.boundarySeq_le_center_of_codim_le_one_seqOn_embeddedDesingPiecesOfNonzero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin ((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.length) {n' c : ℕ} (ψ' : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) (hc : c ≤ 1) (hC : Manifold.IsClosedSubmanifold ψ' (Manifold.IdealSheaf.support (((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.center i)) c) : c = 1 ∧ ∀ (x : ↑↧(((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.stage i.castSucc).carrier), Manifold.IdealSheaf.stalkIdeal (((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.boundarySeq ⊤ i.castSucc) x ≤ Manifold.IdealSheaf.stalkIdeal (((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession.center i) x

Every centre of codimension at most one of a piece lies in the exceptional divisor of its stage, and has codimension one ([Wlo09, Remarks (1) and (2) after Theorem 2.0.3]): the centres lie over Sing(Y) (centersOver_embeddedTriple), have simple normal crossings with the exceptional families (clause (1) of concreteBEDanFamStar_isEmbeddedDesing) and are nonempty (CompatibleFamily.noEmptyCenters); boundarySeq_le_center_of_codim_le_one.

theorem Hironaka.Manifold.isDesingularizedBy_seqOn_embeddedDesingPiecesOfNonzero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (I.restrict U).IsDesingularizedBy ((embeddedDesingPiecesOfNonzero M I hI hI₀).seqOn U hU).toSuccession

Over every relatively compact open the embedded desingularization desingularizes Y (IdealSheaf.IsDesingularizedBy, [Wlo09, Theorem 2.0.2 (1)–(3), (6)]): clauses (1), (2), (3) and (6) of concreteBEDanFamStar_isEmbeddedDesing on the open, (1) read in Hironaka's boundary form and (3) in its transversal form (IsEmbeddedDesing.isProperSnc); the support of the last exceptional divisor is the preimage of Sing(Y): it lies over the centres, hence over Sing(Y), and at a point off it of the preimage of Y the strict transform passes and the composite blow-down is an isomorphism near the point, so the point maps to a simple point of Y exactly when the strict transform, which is smooth, is non-singular there.

theorem Hironaka.Manifold.isDesingularizedBy_embeddedDesingFamOfNonzero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (hI₀ : Manifold.IdealSheaf.IsNonzeroEverywhere I) (K : TopologicalSpace.Compacts M.carrier) : (I.restrict ((embeddedDesingFamOfNonzero M I hI hI₀).nhd K)).IsDesingularizedBy ((embeddedDesingFamOfNonzero M I hI hI₀).seq K)

Over every compact the embedded desingularization desingularizes Y: the case of the neighbourhood of the compact (isDesingularizedBy_seqOn_embeddedDesingPiecesOfNonzero).

The restriction of an ideal sheaf made the unit ideal on its zero components

theorem Hironaka.Manifold.stalkIdeal_restrict_of_mem_zeroLocus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (U : TopologicalSpace.Opens M.carrier) (x : (M.restrict U).carrier) (hx : (M.inclusion U) x ∈ I.zeroLocus) : Manifold.IdealSheaf.stalkIdeal (I.restrict U) x = ⊥

On the preimage of the zero components, the restriction of 𝓘_Y to an open vanishes.

theorem Hironaka.Manifold.stalkIdeal_restrict_unitOnZeroStalks_of_mem_zeroLocus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (U : TopologicalSpace.Opens M.carrier) (x : (M.restrict U).carrier) (hx : (M.inclusion U) x ∈ I.zeroLocus) : Manifold.IdealSheaf.stalkIdeal (I.unitOnZeroStalks.restrict U) x = ⊤

On the preimage of the zero components, the restriction of 𝓘_Y made the unit ideal there is the unit ideal.

theorem Hironaka.Manifold.stalkIdeal_restrict_eq_restrict_unitOnZeroStalks_of_notMem_zeroLocus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (U : TopologicalSpace.Opens M.carrier) (x : (M.restrict U).carrier) (hx : (M.inclusion U) x ∉ I.zeroLocus) : Manifold.IdealSheaf.stalkIdeal (I.restrict U) x = Manifold.IdealSheaf.stalkIdeal (I.unitOnZeroStalks.restrict U) x

Off the preimage of the zero components, the restrictions of 𝓘_Y and of 𝓘_Y made the unit ideal on its zero components agree.

The embedded desingularization of an arbitrary reduced closed subspace

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.embeddedDesingPieces {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : CompatibleFamily (embeddedTriple I.unitOnZeroStalks ⋯)

The pieces of the embedded desingularization of a reduced closed subspace Y: those of 𝓘_Y made the unit ideal on the connected components of M where it vanishes (IdealSheaf.unitOnZeroStalks), which is reduced with nonzero stalks.

Equations

• Hironaka.Manifold.embeddedDesingPieces M I hI = Hironaka.Manifold.embeddedDesingPiecesOfNonzero M I.unitOnZeroStalks ⋯ ⋯

noncomputable def Hironaka.Manifold.embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : M.ExtensionCompatibleFamily

The embedded desingularization of a reduced closed subspace Y as one family over M ([Wlo09, Theorem 2.0.2]): the pieces of Y (embeddedDesingPieces) glued along the exhaustion of M.

Equations

• Hironaka.Manifold.embeddedDesingFam M I hI = Hironaka.Manifold.embeddedDesingFamOfNonzero M I.unitOnZeroStalks ⋯ ⋯

theorem Hironaka.Manifold.isProperMap_embeddedDesingFam_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : IsProperMap ⇑(embeddedDesingFam M I hI).map

The blow-down of the embedded desingularization is proper.

theorem Hironaka.Manifold.isAnalyticIsoOver_embeddedDesingFam_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : (embeddedDesingFam M I hI).map.IsIsoOver (Manifold.IdealSheaf.support I \ I.regularLocus)ᶜ

The blow-down of the embedded desingularization is an isomorphism off Sing(Y): the singular locus of 𝓘_Y made the unit ideal on its zero components is that of Y (support_diff_regularLocus_unitOnZeroStalks).

theorem Hironaka.Manifold.isDesingularizedBy_seqOn_embeddedDesingPieces {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (I.restrict U).IsDesingularizedBy ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession

Over every relatively compact open the embedded desingularization desingularizes Y (IdealSheaf.IsDesingularizedBy, [Wlo09, Theorem 2.0.2 (1)–(3), (6)]): the clauses for 𝓘_Y made the unit ideal on its zero components (isDesingularizedBy_seqOn_embeddedDesingPiecesOfNonzero) transfer to 𝓘_Y (IsDesingularizedBy.of_eq_off_clopen): the two ideal sheaves agree off the clopen set of zero components, where the one is zero and the other the unit ideal, and the centres lie over the singular locus (centersOver_embeddedTriple).

theorem Hironaka.Manifold.isDesingularizedBy_embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (K : TopologicalSpace.Compacts M.carrier) : (I.restrict ((embeddedDesingFam M I hI).nhd K)).IsDesingularizedBy ((embeddedDesingFam M I hI).seq K)

Over every compact the embedded desingularization desingularizes Y: the case of the neighbourhood of the compact (isDesingularizedBy_seqOn_embeddedDesingPieces).

theorem Hironaka.Manifold.center_ne_top_seq_embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (K : TopologicalSpace.Compacts M.carrier) (i : Fin ((embeddedDesingFam M I hI).seq K).length) : ((embeddedDesingFam M I hI).seq K).center i ≠ ⊤

No centre of the succession over a compact is empty: the pieces are produced with the empty blow-ups erased (CompatibleFamily.noEmptyCenters).

theorem Hironaka.Manifold.boundarySeq_le_center_of_codim_le_one_embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (K : TopologicalSpace.Compacts M.carrier) (i : Fin ((embeddedDesingFam M I hI).seq K).length) {n' c : ℕ} (ψ' : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) (hc : c ≤ 1) (hC : Manifold.IsClosedSubmanifold ψ' (Manifold.IdealSheaf.support (((embeddedDesingFam M I hI).seq K).center i)) c) : c = 1 ∧ ∀ (x : ↑↧(((embeddedDesingFam M I hI).seq K).stage i.castSucc).carrier), Manifold.IdealSheaf.stalkIdeal (((embeddedDesingFam M I hI).seq K).boundarySeq ⊤ i.castSucc) x ≤ Manifold.IdealSheaf.stalkIdeal (((embeddedDesingFam M I hI).seq K).center i) x

Every centre of codimension at most one of the succession over a compact lies in the exceptional divisor of its stage, and has codimension one (boundarySeq_le_center_of_codim_le_one_seqOn_embeddedDesingPiecesOfNonzero for 𝓘_Y made the unit ideal on its zero components, whose family the family of 𝓘_Y is).

theorem Hironaka.Manifold.exists_adaptedChart_seqOn_embeddedDesingPieces {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (a : ↑↧(((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.stage (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).carrier) : a ∈ Manifold.IdealSheaf.support (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.strictTransformSubspaceSeq (I.restrict U) (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)) → ∃ (c : ℕ) (φ : OpenPartialHomeomorph (((embeddedDesingPieces M I hI).seqOn U hU).stage (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).length)).carrier (Fin n → 𝕜)) (σ : Fin c ↪ Fin n) (cidx : { j : (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).ι // a ∈ (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).hyp j } → Fin n), Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.IdealSheaf.support (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.strictTransformSubspaceSeq (I.restrict U) (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length))) φ σ ∧ Manifold.HypersurfaceFamily.IsSncChartAt (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)) φ a cidx ∧ ∀ (j : { j : (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).ι // a ∈ (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).hyp j }), cidx j ∉ Set.range ⇑σ

The transversal chart clause (3) with the last exceptional family named: at every point of the last strict transform of Y ∩ U there is a chart adapted to it which is a simple normal crossings chart of the last exceptional family, the coordinates of the strict transform among those of no member (IsEmbeddedDesing.isProperSnc for 𝓘_Y made the unit ideal on its zero components, transferred by exists_adaptedChart_strictTransformSubspaceSeq_of_eq_off_clopen).

theorem Hironaka.Manifold.exists_monomial_seqOn_embeddedDesingPieces {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (x : (((embeddedDesingPieces M I hI).seqOn U hU).stage (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).length)).carrier) : ∃ (s : Finset (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).ι) (α : (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).ι → ℕ), (∀ j ∈ s, x ∈ (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).hyp j) ∧ (Manifold.IdealSheaf.pullback ⇑((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.composite ⋯ (I.restrict U)).stalkIdeal x = Manifold.IdealSheaf.stalkIdeal (((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.strictTransformSubspaceSeq (I.restrict U) (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)) x * ∏ j ∈ s, Manifold.vanishingStalk ((((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.totalTransformSeq (Fin.last ((embeddedDesingPieces M I hI).seqOn U hU).toSuccession.length)).hyp j) x ^ α j

The monomial clause (6) with the last exceptional family named: at every point of the last stage, σ^*(𝓘_Y) = I_Ỹ · ∏ I_{E^j}^{α_j} over the members of the last exceptional family through the point (clause (6) of concreteBEDanFamStar_isEmbeddedDesing for 𝓘_Y made the unit ideal on its zero components, transferred by exists_monomial_strictTransformSubspaceSeq_of_eq_off_clopen).

theorem Hironaka.Manifold.isPullbackUpToEmptyAlong_embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (J : N.IdealSheaf) (hJ : J.IsReduced) (hIJ : J = Manifold.IdealSheaf.pullback ⇑g ⋯ I) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) (hK : ⇑g '' ↑((embeddedDesingFam N J hJ).nhd K') ⊆ ↑((embeddedDesingFam M I hI).nhd K)) : ((embeddedDesingFam N J hJ).seq K').IsPullbackUpToEmptyAlong ((embeddedDesingFam M I hI).seq K) g

The embedded desingularization on the standard model commutes with local analytic isomorphisms, over every pair of compacts ([Wlo09, Theorem 2.0.2 (4)]; the form of [Wlo09, Theorem 3.5.1 (2)]): for a local analytic isomorphism g : N → M and J = g^* I, the succession over U_{K'} is the pull-back along g of the succession over U_K up to empty blow-ups whenever g(U_{K'}) ⊆ U_K. The triple of J made the unit ideal on its zero components carries the pull-back data of that of I (unitOnZeroStalks_pullback_of_isLocalDiffeomorph), so the values of the functor correspond (CommutesWithLocalIsos), and CompatibleFamily.isPullbackUpToEmptyAlong_seqOn reads the pull-back predicate.