The total transform of the value is the strict transform times an exceptional monomial

Clause (6) of [Wlo09, Theorem 2.0.2], the strengthening of Bravo–Villamayor: the pull-back of the ideal of Y to the last stage is 𝓘_Ỹ · 𝓘_Ẽ, with Ỹ the strict transform and Ẽ a simple normal crossing divisor which is a locally finite combination of the components of the exceptional divisor. It is proved here for the value of the embedded desingularization functor bedanFamOfInput bmod n over a relatively compact open U, at every point x of the last stage: the stalk of the pulled-back ideal is the stalk of the final strict transform times a monomial in the vanishing ideals of the exceptional components through x, with exponents chosen at x. The theorem carries the explicit hypothesis hsat of Hironaka/Resolution/Analytic/Wlo09/StrictTransformClauses.lean (local generators for the saturation stalks at every stage), which always holds; the assembly of BEDanFamStarOfInput_isEmbeddedDesing uses the present form directly.

Proof. Along a blow-up sequence of order ≥ 1 for (𝓘, 1), the pull-back of 𝓘 to stage i is the marked transform times the ideal of an exceptional divisor with simple normal crossings, σ_i^* ⋯ σ_1^*(𝓘_0) = 𝓘_i · 𝓘(E_i) with 𝓘(E_i) = σ_i^*(𝓘(E_{i−1})) · 𝓘(D_i) (the induction in the proof of [Wlo09, Proposition 4.0.2, (1)⇒(2)]); Kollár writes the pull-back as the ideal of an explicit divisor supported on the total transforms of the exceptional divisors [Kol07, 72]. The formula is proved stage by stage as FiniteSuccession.isBoundaryMonomialAt_stageMapAux (Hironaka/Resolution/Analytic/Principalization/MonomialSeq.lean): the pull-back of 𝓘 to the last stage is a boundary monomial in the total transform of the boundary with residual the final marked transform 𝓘_r. On DomBEDan the boundary of T|_U has no member, so the total transform grown from it is the exceptional family totalTransformSeq up to the relabelling of Hironaka/Resolution/Analytic/Wlo09/BoundaryBridge.lean (exists_equiv_totalTransformSeqFrom_of_isEmpty), along which the finite set of components and the exponents transport (Finset.map, Finset.prod_map); and 𝓘_r = Ỹ by bedanFamOfInput_strictTransform_eq_of_hsat.

theorem Hironaka.Manifold.bedanFamOfInput_totalTransform_eq_of_hsat (𝕜 : 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)) (hsat : ∀ (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length), Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I i.castSucc))) (x : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stage (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).carrier) : ∃ (s : Finset ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).ι) (α : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).ι → ℕ), (∀ j ∈ s, x ∈ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).hyp j) ∧ (Manifold.IdealSheaf.pullback ⇑((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stageMap (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)) ⋯ (T.pullback (M.inclusion U) ⋯).I).stalkIdeal x = Manifold.IdealSheaf.stalkIdeal ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)) x * ∏ j ∈ s, Manifold.vanishingStalk (((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).hyp j) x ^ α j

Clause (6) of [Wlo09, Theorem 2.0.2] for the value of bedanFamOfInput bmod n over U, under hsat: on the last stage, at every point the pulled-back ideal is the final strict transform's ideal times a monomial in the vanishing ideals of the exceptional components through the point, with the exponents chosen at the point. Kollár's formula for the pull-back at mark 1 [Kol07, 72] (isBoundaryMonomialAt_stageMapAux), with the residual identified by bedanFamOfInput_strictTransform_eq_of_hsat and the boundary read through the empty-boundary bridge.