Step 2 of order reduction is indifferent to empty boundary members #
Kollár's convention [Kol07, 32] and the reindexing of [Kol07, 34.1]: deleting unit-ideal members of
the boundary changes nothing. This module proves it for the maximal-contact case of
[Kol07, Theorem 103] (Hironaka.BO.maxContactCase, Steps 1–2 of the proof) under two hypotheses
on the boundary-clearing data of [Kol07, Lemma 102] at every mark: hind, the rounds at matched
positions agree (BDFamily.IndifferentToEmptyMembers), and hnil, the round of a unit member is
nil (BDFamily.NilAtUnitMember,
Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferentFunctor.lean). Both hold for the
boundary-clearing data of Hironaka/Resolution/Algebraic/BoundaryClearing/.
- Step 2.1 ([Kol07, 104, Step 2.1];
step21Seq, one round per member in order): by induction on the positionjof the larger boundaryE, the sequence afterjrounds equals the sequence of the smaller boundaryE'aftererasureCount E E' e jrounds, the number of members ofE'whose partner sits below positionj. A deleted member's round isnil(hnil: its transform is the unit ideal at every stage,strictTransformSeq_top); a surviving member's round is the partner's round (hindat the matched positions, the deletion carried to the induced boundaries byexists_isTopErasure_totalTransformSeqand the positions bymonoEquivOfFin_totalTransformSeq_of_lt); at the end the counts are the sizes (erasureCount_card). - Step 2.2 ([Kol07, 104, Step 2.2];
step22): the exceptional sub-families of the two boundaries at the end of the common Step 2.1 sequence agree up to a surjective order embedding (exists_orderEmbedding_exceptionalFamily), so the two Step 2.2 input triples(X_r, I_r, F_r + H_r)differ by a deletion of no members, andhindat the marks(m), at the positionscard F_r.ιandcard F'_r.ι(monoEquivOfFin_lex_inr_last), identifies the values through the re-tuning (step22Functor_seq_of_maxOrd_eq); below the mark both arenil. maxContactCase_indifferentToEmptyMembersconcludes through the case split ofmaxContactCaseonmax-ord I.
The abbreviation Triple.withBoundary used throughout is defined in
Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferentFunctor.lean. The globalised functor
is treated in Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferentGlobal.lean.
Counting the surviving positions #
The number of members of E' whose partner in E along e sits at a position below j: the
number of Step 2.1 rounds of (X, I, E') matched by the first j rounds of (X, I, E). Not in
the sources; it makes the reindexing of [Kol07, 34.1] explicit.
Equations
- Hironaka.BO.erasureCount E E' e j = Fintype.card { a : E'.ι // ↑((monoEquivOfFin E.ι ⋯).symm (e a)) < j }
Instances For
A position of E outside the range of e (a deleted member) adds no matched round.
At a matched position j = e i', the count is the position of i' in E'.
After a matched position j = e i', the count is the position of i' in E' plus one.
After all positions of E, every member of E' is matched.
Step 2.1 #
At the end of any smooth blow-up sequence of order m, the member at a deleted position of
E is the unit ideal, being its birational transform (component_originalIdx,
strictTransformSeq_top).
The rounds of the boundary-clearing data at matched positions of the two induced boundaries
agree: hind on the triple induced by the common sequence, with the deletion carried to the
induced boundaries (exists_isTopErasure_totalTransformSeq) and the positions by
monoEquivOfFin_totalTransformSeq_of_lt.
The inductive step at a matched position, on the whole Step 2.1 values: equal sequences after
j and j' rounds give equal sequences after the next round.
The Step 2.1 sequence of (X, I, E) after j rounds is the Step 2.1 sequence of (X, I, E')
after the matched number of rounds ([Kol07, 104, Step 2.1] with the conventions [Kol07, 32] and
[Kol07, 34.1]): a deleted member's round is nil (hnil), a surviving member's round is its
partner's (hind).
Step 2.2 and Step 2 #
Step 2.2 on the two input triples built from the same Step 2.1 sequence agree
([Kol07, 104, Step 2.2] with the reindexing of [Kol07, 34.1]): their boundaries F_r + H_r and
F'_r + H_r are matched by a surjective order embedding, no member being deleted
(exists_orderEmbedding_exceptionalFamily), so hind at the mark s(m) identifies the re-tuned
values at the positions of H_r; below the mark both are nil.
Step 2 on (X, I, E'), generalised over its Step 2.1 sequence S₂ with S₂ equal to the
Step 2.1 sequence of (X, I, E): it is Step 2 on (X, I, E).
Step 2 of the proof of [Kol07, Theorem 103] on (X, I, E) and on (X, I, E') agree, for E'
obtained from E by deleting unit members ([Kol07, 104, Steps 2.1–2.2] with the conventions
[Kol07, 32] and [Kol07, 34.1]).
The maximal-contact case #
The maximal-contact case of [Kol07, Theorem 103] is indifferent to empty boundary members
([Kol07, 32] and the reindexing of [Kol07, 34.1] for Steps 1–2 of the proof): for a triple of
BOClass n m with a smooth hypersurface H of maximal contact, and boundary-clearing data at every
mark that are indifferent to empty members (hind) and nil at a unit member (hnil), deleting
unit members of E does not change BO^H_{n,m}(X, I, E). Through the case split of
maxContactCase: at the mark, Step 2 on the tuned triples (step2Seq_indifferent; tuning keeps
E); below the mark both values are nil.