The nonmonomial part at the generic point of a strict transform #
The hypothesis of Włodarczyk's Claim in the proof of [Wlo05, Theorem 4.7.1]: I = I_{Y₁} near a
generic point η of Y₁, η on no member of the boundary. Before the first centre containing the
strict transform c̃ of c = I_{Y₁} (the proof of [Kol07, Corollary 22]) the stage map is an
isomorphism on stalks at the generic point η̃ of c̃, and no exceptional or boundary component
passes through η̃ (isIso_stalkMap_stageMap_of_forall_notMem,
notMem_support_totalTransformSeq_of_forall_notMem). So the monomial part is the unit ideal at
η̃, the nonmonomial part is the marked transform itself, and its stalk is the image of
I_η = 𝔪_η under the isomorphism: N(I_i)_{η̃} = 𝔪_{η̃}, of order 1 (ord_maximalIdeal_eq_one;
I is nonzero at η). Together with not_centerContains_of_leOrdAlong_two
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimTools) this places the first containing centre
in the round of order 1 of Step 1 of the proof of [Kol07, Theorem 107]. Used in
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedGenericLift and
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimStep1.
The hypothesis of Włodarczyk's Claim transported to a stage before the first containing centre:
at a point η' over η lying over no earlier centre, the marked transform (of any mark) of an
ideal sheaf J agreeing with vanishingIdeal (closure {η}) at η has the maximal ideal as its
stalk — the image of J_η = 𝔪_η under the stalk isomorphism of the stage map.
Under the hypotheses of stalkIdeal_markedTransformSeq_eq_maximalIdeal, with J nonzero at
η, the marked transform has order exactly 1 at η' ([Kol07, Definition 47] at the generic
point) — its stalk is the maximal ideal, nonzero since it is the image of J_η ≠ 0 under an
isomorphism.
The monomial part of any ideal sheaf at a point over η ∉ E lying over no earlier centre is
the unit ideal: no member of the total transform of E passes through the point.
The nonmonomial part of the marked transform of I at a point over η ∉ E lying over no
earlier centre, with respect to the total transform of E, has the maximal ideal as its stalk —
the monomial part is the unit ideal there (stalkIdeal_monomialPart_totalTransformSeq_eq_top) and
the marked transform's stalk is the maximal ideal
(stalkIdeal_markedTransformSeq_eq_maximalIdeal).
Under the hypotheses of stalkIdeal_nonmonomialPart_markedTransformSeq_eq_maximalIdeal, with
I nonzero at η, the nonmonomial part of the marked transform has order exactly 1 at η'
([Kol07, Definition 47] at the generic point) — its stalk is the maximal ideal, nonzero since it is
the image of I_η ≠ 0 under an isomorphism.
The hypothesis of Włodarczyk's Claim along the run of BMO_1 (the proof of
[Kol07, Corollary 22]): for a marked triple T, a point η on no member of T.E at which T.I
agrees with c := vanishingIdeal (closure {η}), and a stage i of the run of BMO_1 on T at or
before the first centre containing the strict transform of c, that strict transform has a
generic point η' over η at which the nonmonomial part of the induced marked ideal has order
1.