Canonicity of the rounds, compatibility, and the resolution family #
The value of the rounds of the resolution family on a relatively compact open U does not depend
on the admissible chain along which they are read (resolveSeqOnAlong_chain_indep), the values on
U ≤ V are compatible under restriction up to empty blow-ups (resolveSeqOn_compat), and the
family resolveFam : CompatibleFamily T is assembled with that compat field. This is the
compatibility clause of Włodarczyk's locally finite principalization [Wlo09, Theorem 2.0.3 (4)];
on the side of the functors it is the behaviour of a blow-up sequence functor under smooth
morphisms [Kol07, 34.1] together with the remark after [Kol07, Theorem 68] that the rounds above
the order bound are empty.
The proof rests on Resolve/{Comp,EmptyRound,Transport,TopRound,Indiff}.lean. Two admissible
chains of the same length, one inside the other, have the same value: eraseEmpty_resolveFrom_congr
along the inclusion of the outermost opens, the identity on U, and pullback_id
(resolveSeqOnAlong_eq_of_le). A chain one round longer than a chain inside it has the same value:
its top round has no centre over the shorter chain's outermost open, where the order is below the
round's mark, so eraseEmpty_resolveFrom_succ_eq_restrict drops it (the low-order chain being the
shorter chain's opens traced on the longer one's outermost open), and eraseEmpty_resolveFrom_congr
along restrictMap carries the rounds from that region, an open of an open, to the shorter chain's
outermost open (resolveSeqOnAlong_eq_of_succ; the closure hypothesis comes from
closure U ⊆ W 1 ⊆ W m, so one round must remain). The bridge from an arbitrary chain c to the
canonical one is c.shrunk: c cut down by the iterated shrinks of closure U inside
{ord ≤ d_U} (shrinkChain), of any length m between d_U and c.D; every one of its opens
has order ≤ d_U, so every truncation is admissible. Then (resolveSeqOnAlong_eq_canonical): a
chain with no round has the order vanishing on U, and both values are empty by
eraseEmpty_resolveFrom_eq_nil_of_ord_eq_zero; otherwise d_U ≤ c.D since closure U lies in
the outermost open, c equals its cut-down of full length, the cut-downs of consecutive lengths
agree (the same lemma at the last drop, from one round to none, when d_U = 0), and the cut-down
of length d_U lies inside the canonical chain. Canonicity is two applications; compatibility
reads the canonical chain of V as a chain for U, whose reading map is the reading map of V
after the inclusion U ≤ V: canonicity, resolveFrom_congr_ι, resolveFrom_comp and
eraseEmpty_pullback_eraseEmpty.
resolveSeqOnAlong_eq_of_le,resolveSeqOnAlong_eq_of_succ: the two comparison lemmas.ResolveChain.shrunk,ResolveChain.ord_le_maxOrdOn_of_mem_shrunk,maxOrdOn_le,resolveSeqOnAlong_eq_nil_of_ord_eq_zero: the cut-down chain, the order bound, the empty value of a chain with no round.resolveSeqOnAlong_eq_canonical: every admissible chain has the canonical value.resolveSeqOnAlong_chain_indep,resolveSeqOn_compat,resolveFam.
Lemma A: nested chains of the same length #
Two admissible chains of the same length, one inside the other, have the same value
([Kol07, 34.1]; [Wlo09, Theorem 2.0.3 (4)]): eraseEmpty_resolveFrom_congr along the inclusion of
the outermost opens (restrictLE), the identity on U, and pullback_id.
Lemma B: dropping the top round of a chain one longer #
A chain one round longer than a chain inside it has the same value (the remark after
[Kol07, Theorem 68]). The top round has no centre over the shorter chain's outermost open, where
the order is below the round's mark: eraseEmpty_resolveFrom_succ_eq_restrict drops it (the
low-order chain is the shorter chain's opens traced on the longer one's outermost open; its
closure hypothesis is closure U ⊆ W 1 ⊆ W m, whence one round must remain), and
eraseEmpty_resolveFrom_congr along restrictMap carries the rounds from that region, an open of
an open, to the shorter chain's outermost open.
The chain cut down by the shrinks of closure U inside {ord ≤ d_U} #
The chain c cut down by the iterated shrinks of closure U inside {ord ≤ d_U} (the
k-th open is c.W k ⊓ shrinkChain … (c.D - k)), of any length m between d_U and c.D: the
compact closures and the shrinking are inherited, U lies in the innermost open, and every open
has order ≤ d_U, so every truncation is admissible. The bridge from an arbitrary admissible chain
to the canonical one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The order on every open of the cut-down chain is at most d_U (its opens lie in the shrinks,
which lie in {ord ≤ d_U}).
d_U is the least bound (bddAbove_ord_on_compact, Nat.find): any bound of the order on
closure U is at least d_U.
The value along a chain is empty when the order vanishes on U
(eraseEmpty_resolveFrom_eq_nil_of_ord_eq_zero at the chain's outer triple; the remark after
[Kol07, Theorem 68]).
Canonicity #
Every admissible chain has the canonical chain's value ([Wlo09, Theorem 2.0.3 (4)];
[Kol07, 34.1]). A chain with no round has the order vanishing on U, and both values are empty
(resolveSeqOnAlong_eq_nil_of_ord_eq_zero). Otherwise d_U ≤ c.D, since closure U lies in the
outermost open; the chain equals its cut-down of full length (resolveSeqOnAlong_eq_of_le), the
cut-downs of consecutive lengths agree (resolveSeqOnAlong_eq_of_succ; the empty value at the
last drop, from one round to none, when d_U = 0), and the cut-down of length d_U lies inside
the canonical chain.
Canonicity ([Wlo09, Theorem 2.0.3 (4)]; [Kol07, 34.1], with the remark after
[Kol07, Theorem 68] for the empty rounds above the order bound): the value on U does not depend
on the admissible chain; two chains for U, of any lengths, give the same list. Both have the
canonical chain's value (resolveSeqOnAlong_eq_canonical; closure U is compact, inside the
closure of a chain's innermost open).
Compatibility and the resolution family #
The compat field of the resolution family ([Wlo09, Theorem 2.0.3 (4)]; the shape of
CompatibleFamily.compat): for U ≤ V the value on U is the pull-back of the value on V along
the open inclusion, with the empty blow-ups erased. The canonical chain of V is an admissible
chain for U whose reading map is the reading map of V after the inclusion U ≤ V: canonicity
(resolveSeqOnAlong_chain_indep), resolveFrom_congr_ι, resolveFrom_comp and
eraseEmpty_pullback_eraseEmpty.
The resolution family of the triple T ([Hir64, Main Theorem II(N), p. 176], order
reduction iterated at decreasing maximal order; [Wlo09, Theorem 2.0.3 (1), (4)]; the remark after
[BM97, Theorem 1.6] on non-compact spaces): the compatible family whose value on a relatively
compact open U is resolveSeqOn bo T U hU, without empty centres, with the compat field
resolveSeqOn_compat.
Equations
- Hironaka.Manifold.resolveFam bo T = { seqOn := Hironaka.Manifold.resolveSeqOn bo T, noEmptyCenters := ⋯, compat := ⋯ }