The assembly of the analytic embedded desingularization

The clauses of [Wlo09, Theorem 2.0.2] for the embedded desingularization functor bedanFamOfInput 𝕜 bmod n of Hironaka/Resolution/Analytic/Wlo09/Basic.lean, assembled into BEDanFamStar.IsEmbeddedDesing for the all-dimensions functor BEDanFamStarOfInput 𝕜 bmod hbmod of Hironaka/Resolution/Analytic/Wlo09/Functoriality.lean.

• BEDanFam_center_disjoint_reg: clause (2) of [Wlo09, Theorem 2.0.2] ("all centers C_i are disjoint from the set Reg(Y) of points where Y is smooth"; the centres lie in the support by [Wlo09, Definition 3.2.4 (1)], and the stop rule of the proof of [Wlo09, Theorem 7.4.1] applies at a smooth point): no point of any centre lies over a simple point of Y ∩ U. From the local analysis bedanFamOfInput_center_disjoint_fiber_near_regular (Hironaka/Resolution/Analytic/Wlo09/Clauses.lean) and the locality of regularLocus (exists_opens_reg_of_mem_reg, Hironaka/Resolution/Analytic/Wlo09/RegLocality.lean).
• BEDanFamStarOfInput_isEmbeddedDesing: the assembly. Clause (1) is bedanFamOfInput_isSnc_totalTransformSeq and bedanFamOfInput_hasSncWith_center (Clauses.lean); clause (2) is the theorem above; clause (3), the smoothness of the final strict transform and its simple normal crossings with the exceptional divisor, is bedanFamOfInput_isNonsingular_strictTransform_of_hsat and bedanFamOfInput_exists_adaptedChart_isSncChartAt_of_hsat (StrictTransformClauses.lean) with the finite-type hypothesis discharged by saturationStalk_hasLocalGenerators; clause (6), the total transform formula σ^*(I_Y) = I_Ỹ · I_Ẽ, is bedanFamOfInput_totalTransform_eq_of_hsat (TotalTransformClause.lean); clause (4), the commutation with local analytic isomorphisms, is the field commutesWithLocalIsos of the modified marked resolution restricted to the class (CommutesWithLocalIsos.restrictDomain), read through BEDanFamStarOfInput_fam (rfl); clause (5), the compatibility of the values under restriction U₁ ≤ U₂, is the field compat of the compatible family itself.

This module constructs nothing; it assembles the theorems of the directory. The concrete instance is concreteBEDanFamStar_isEmbeddedDesing in Hironaka/Resolution/Analytic/Wlo09/Concrete.lean.

theorem Hironaka.Manifold.BEDanFam_center_disjoint_reg (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (n : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length) (x : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stage i.castSucc).carrier) (hx : x ∈ Manifold.IdealSheaf.support ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.center i)) : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stageMap i.castSucc) x ∉ (fun (y : ↑↑(T.pullback (M.inclusion U) ⋯).I.toAnalyticSpace.toPresheafedSpace) => ↑(T.pullback (M.inclusion U) ⋯).I.toAnalyticSpaceι y) '' (T.pullback (M.inclusion U) ⋯).I.toAnalyticSpace.regularLocus

Clause (2) of [Wlo09, Theorem 2.0.2] for the embedded desingularization functor bedanFamOfInput 𝕜 bmod n: no point of any centre of the embedded desingularization of Y ∩ U lies over a simple point of Y ∩ U. From the local analysis bedanFamOfInput_center_disjoint_fiber_near_regular (no centre over an open on which Y is non-singular) and the locality of regularLocus: a simple point has an open neighbourhood V in the ambient manifold on which Y is non-singular.

theorem Hironaka.Manifold.BEDanFamStarOfInput_isEmbeddedDesing (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (hbmod : ∀ (n s : ℕ), (bmod n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmod (n - s)).functor) : BEDanFamStar.IsEmbeddedDesing 𝕜 (BEDanFamStarOfInput 𝕜 bmod hbmod)

The embedded desingularization theorem for BEDanFamStarOfInput [Wlo09, Theorem 2.0.2]: the assembly of IsEmbeddedDesing from the clauses proved in this directory: (1) bedanFamOfInput_isSnc_totalTransformSeq and bedanFamOfInput_hasSncWith_center; (2) BEDanFam_center_disjoint_reg; (3) the smoothness and simple normal crossings of the final strict transform, with the finite-type hypothesis discharged by saturationStalk_hasLocalGenerators; (6) the total transform formula bedanFamOfInput_totalTransform_eq_of_hsat; (4) the commutation with local analytic isomorphisms, the field of the modified marked resolution restricted to the class (CommutesWithLocalIsos.restrictDomain).