Dropping an empty top round #
Kollár's remark after [Kol07, Theorem 68], that the order reduction does nothing when
max-ord I < m, for the rounds of the resolution family
(Hironaka/Resolution/Analytic/Wlo09/Rounds.lean): when the order of cur is ≤ d on a low-order
chain ΩZ inside the chain Ω, containing the reading image, the rounds from d + 1 along Ω,
read through ι, agree up to empty blow-ups with the rounds from d on the restriction of cur to
the outer open ΩZ d, along the traced chain, read through the corestricted ι
(eraseEmpty_resolveFrom_succ_eq_restrict). Canonicity
(Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean) uses it to bring an admissible chain of any
length down to the canonical one.
The proof is bookkeeping on the lemmas of Hironaka/Resolution/Analytic/Wlo09/EmptyRound.lean,
Hironaka/Resolution/Analytic/Wlo09/Indiff.lean and
Hironaka/Resolution/Analytic/Wlo09/Transport.lean. The top round BO_{n,d+1} at Ω d has no
centre over a point of order ≤ d (the field isOfOrderGe), so its list erases to nil both on
the reading manifold and over the region Z' := ΩZ d ∩ Ω d of the round's open
(eraseEmpty_pullback_roundList_eq_nil, twice). Two identifications follow from
eraseEmptyTransport with the empty list: θ, of the round's last stage over the reading manifold
with the reading manifold itself, and τ, of the round's last stage over the region with the
region, both over the identity of the base (stageMap_last_toAnalyticMap_eraseEmptyTransport), so
the lifted reading map is the corestricted reading map up to θ and τ (eq_of_stageMap_last_eq,
uniqueness of maps over the blow-down). Along τ the derived ideal is the restricted ideal
(markedTransformSeq_last_pullbackLiftLast, markedTransformSeq_last_eraseEmptyTransport) and the
restricted boundary is an empty subfamily of the derived boundary
(exists_orderEmbedding_eraseEmptyTransport), whose empty members resolveFrom_indiff removes.
Then eraseEmpty_resolveFrom_congr transports three times: from the round's last stage to the last
stage over the region (the exact pull-back along kZ, the lift of the region's inclusion), from
that last stage to the region along τ, and from the region, an open of the open Ω d, to the
restriction of X to ΩZ d along restrictMap. eraseEmpty_concat_congr with the empty first
piece on the right assembles the top round and the rest.
The hypotheses hordZ, hfinZ, hΩZ', hΩZsub', hrangeZ' restate hZord, hfin, hΩZ,
hΩZsub, hrangeZ on the restricted data; they are the data of the right-hand side, which the
caller supplies. The hypothesis hclosure (the closure of the reading image inside ΩZ d) is used
only through subset_closure; hrZ gives the same.
HypersurfaceFamily.finite_nonempty_comap: finitely many nonempty members survive an inverse image.eraseEmpty_resolveFrom_succ_eq_restrict: the theorem.
Finitely many nonempty members of a family stay finitely many after an inverse image: an empty
member pulls back to an empty member (the finiteness clause of BOClass).
Dropping an empty top round (the remark after [Kol07, Theorem 68]). If the order is ≤ d on
the closure of the reading image, the rounds from d + 1 read through ι agree up to empty
blow-ups with the rounds from d on the restriction of cur to the outer open ΩZ d of any
admissible low-order chain ΩZ of opens of X (compact closures, shrinking, ΩZ k ≤ Ω k,
ord ≤ d on ΩZ d, the reading image in ΩZ 0), read through the corestricted ι. Proof:
eraseEmpty_pullback_roundList_eq_nil empties the top round over the reading image and over the
region ΩZ d ∩ Ω d of the round's open; the derived triple over the region is the restricted
triple up to the transport τ along the empty erasure (the derived ideal by
markedTransformSeq_last_eraseEmptyTransport, the restricted boundary an empty subfamily of the
derived one, whose empty members resolveFrom_indiff removes); eraseEmpty_resolveFrom_congr
transports three times (to the last stage over the region, along τ, and from the open of an open
to X.restrict (ΩZ d)).