The remaining members after an isolation #
In the isolation passage of the proof of [Wlo05, Theorem 4.7.1], after the isolation the modified
run restarts on (X_n, I_n : I_Γ, E_n) with the remaining components. This module shows that the
invariant InvCE of the loop (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses) holds again
for the strict transforms of the members not absorbed at the absorbing stage: each has a generic
point η' over the member's generic point (the proof of [Kol07, Corollary 22]: the blow-ups are
local isomorphisms at the generic point before the first containing centre), lying on no member of
the boundary, off the absorbed strict transforms, so that the colon by I_Γ changes nothing at η'
and the isolated ideal agrees there with the strict transform, which is the reduced ideal of the
closure of η'; and η' is a generic point of the support of the isolated ideal. The remaining
strict transforms are disjoint from the absorbed ones.
The disjointness from the absorbed strict transforms is a hypothesis of the general form
exists_genericPoint_isolatedMarkedIdeal_of_not_absorbed_of_disjoint, discharged here from
ClaimKC (a CONDITIONAL lemma, since ClaimKC is false) and unconditionally from CP1 in
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Remaining. Used in
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedIsolatedState,
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Remaining,
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry and
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Absorbed.
The data of a member not absorbed at the stage of the loop: the invariant of the loop gives its
generic point η, off the boundary, at which T.I agrees with it; the stop rule gives no
absorption before the stage of the loop.
A member not absorbed at the stage of the loop has its strict transform disjoint from every
absorbed one (the disjointness of [Wlo05, Theorem 4.7.1] for the loop; conditional on
ClaimKC).
The invariant is restored for a remaining member, with the disjointness from the absorbed
strict transforms as a hypothesis (the proof of [Kol07, Corollary 22]): the strict transform of a
member not absorbed at the stage of the loop is the reduced ideal of the closure of a generic
point η' of the support of the isolated ideal, lying on no member of the boundary, at which the
isolated ideal agrees with it.
The invariant is restored for a remaining member (the proof of [Kol07, Corollary 22];
conditional on ClaimKC, which supplies the disjointness): the strict transform of a member not
absorbed at the stage of the loop is the reduced ideal of the closure of a generic point η' of
the support of the isolated ideal, lying on no member of the boundary, at which the isolated ideal
agrees with it.
The strict transform at the stage of the loop determines the member (the proof of [Kol07, Corollary 22]): two members with the same strict transform have the same generic point, the unique point over it being the generic point of the strict transform.