One round of the loop #
The definition of BED (Hironaka.Resolution.Algebraic.Wlo05.Embedded) writes a round of the loop
as the run truncated before the absorbing stage n, glued to the loop restarted on the isolated
triple (isolatedTriple T hm C n, the marked triple induced at the end of the truncation with its
ideal enlarged to the colon by the absorbed components) with the remaining members
(remainingComponents T hm C n). Both are read through the truncation run.take n at its
Fin.last; the facts of the isolation are read at the stage n of the run
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedIsolatedState). This module:
- carries the state of the loop across the cast of the truncation
(
embeddedStateData_isolatedTriple): the invariant holds for the isolated triple with the remaining members and the protected componentsprotectedTake(the previously protected ones and the absorbed ones, transported to the end of the truncation); - derives the end result of a round from the end result of the restarted loop
(
embeddedEnd_concat_of_isolated): the marked transform along the glued sequence is the marked transform ofI_n = (I_n : I_Γ) · I_Γalong the restarted loop — the marked transform of the isolated ideal times the pull-back ofI_Γ(markedTransformSeq_mul_comap_last_of_isOrderGeSeq); the first is the product of the final strict transforms of the remaining members (the end result of the restarted loop), the second the product of those of the absorbed members (their ideals pull back to their strict transforms, being protected); simple normal crossings and disjointness pass through the restarted loop, the protected components and the members mapping into the members and protected components of the restarted loop.
The concatenation is that of [Kol07, Definition 29] and the marked transform that of
[Kol07, Definition 60]. The two theorems assume ClaimKC, StratumBlowUp and
CentersInNonmonomialSupportOrStratum (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses;
the first is false, the other two unproved) and are CONDITIONAL lemmas; the definitions and the cast
lemmas are used unconditionally by Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Remaining. The
proof of the theorem passes through the loop by CP5 and CP6 instead
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop).
The protected components at the isolated triple: the strict transforms, along the truncated run, of the previously protected components and of the members absorbed at the stage of the loop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The end result of the truncation is the stage Nat.find h of the run.
The strict transforms along the truncation, heterogeneously, are those at the stage of the run.
The ideal of the isolated triple, unfolded: the colon of the marked transform along the
truncation by the reduced ideal of the union of the absorbed strict transforms (the definition,
with the mark 1).
The boundary of the isolated triple, unfolded: the total transform along the truncation.
The ideal of the isolated triple, heterogeneously, is the isolated marked ideal in index form.
The boundary of the isolated triple, heterogeneously, is the total transform at the stage of the run.
The state of the loop holds for the isolated triple, the remaining members and the
protected components at the end of the truncation (the isolation passage of the proof of
[Wlo05, Theorem 4.7.1]); conditional on ClaimKC, StratumBlowUp and
CentersInNonmonomialSupportOrStratum.
The strict transform along the truncated run determines the member (the proof of [Kol07, Corollary 22] on the truncation).
A member or protected component maps into the remaining members or the protected components of the isolated triple.
One round of the loop (the passes of the proof of [Wlo05, Theorem 4.7.1] compose): the end
result of the truncated run glued to a sequence S' on the isolated triple, of order ≥ 1 for
the isolated ideal, whose end result satisfies the conclusions of the loop for the remaining
members and the protected components, satisfies the conclusions of the loop for the original
members and protected components. Conditional on ClaimKC, StratumBlowUp and
CentersInNonmonomialSupportOrStratum.