The absorbed strict transform meets no other member, under Włodarczyk's Claim

Włodarczyk's [Wlo05, Theorem 4.7.1] asserts that the strict transforms Ỹᵢ of the components are "smooth and disjoint". With Włodarczyk's Claim (the proposition ClaimKC of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses, false for the order of the steps of BMO_1 used here), the disjointness would follow: the nonmonomial part N(I_n) agrees with the absorbed strict transform c̃ at the points of c̃; another member's strict transform c̃' lies in the support of N(I_n) (its generic point carries the proper stalk of the marked ideal and lies off the boundary, where M(I_n) is trivial), so at a common point p, c̃_p = N(I_n)_p ≤ c̃'_p; generizing to the generic point of c̃' puts it on c̃, hence the generic points of the two members are related by specialization on X — and two generic points of supp I so related coincide. This gives at once the disjointness of the strict transforms absorbed at the same stage and the fact that a remaining member misses the absorbed ones. This module proves the statement CONDITIONALLY on ClaimKC; the unconditional disjointness is part of the statement CP1 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Absorbed, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry). The unconditional first lemma, stalkIdeal_monomialPart_eq_top_of_forall_notMem (the monomial part of Kol07, Definition–Lemma 110 is trivial off the boundary), is used elsewhere.

theorem Hironaka.Resolution.stalkIdeal_monomialPart_eq_top_of_forall_notMem {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (I : X.IdealSheafData) (E : X.DivisorFamily) {x : ↥X} (hx : ∀ (i : E.ι), x ∉ (E.component i).support) : (BMO.monomialPart I E).stalkIdeal x = ⊤

Off the boundary the fine monomial part has the unit stalk: every factor is the reduced ideal of a component of a member, whose stalk at a point off that member is the unit ideal.

theorem Hironaka.Resolution.eq_of_mem_strictTransformSeq_support_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {η η' : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (hη' : η' ∈ T.I.support.genericPoints) (hηE' : ∀ (i : T.E.ι), η' ∉ (T.E.component i).support) (hIc' : T.I.stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η') (n : Fin (bmoOneRun T hm).length) (habs : CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ↑n) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) (hfirst' : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})) m) (hKC : ClaimKC k) {p : ↥((bmoOneRun T hm).stage n.castSucc)} (hp : p ∈ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).support) (hp' : p ∈ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})) n.castSucc).support) : η = η'

Under the hypothesis ClaimKC (Włodarczyk's Claim; false for the transcribed order): a member absorbed at stage n and any member not absorbed before n have strict transforms meeting at a point only if they are the same member — their generic points coincide ([Wlo05, Theorem 4.7.1]: the strict transforms are disjoint).