Transport of the rounds along a local analytic isomorphism #
The rounds of the resolution family (resolveFrom,
Hironaka/Resolution/Analytic/Wlo09/Rounds.lean) on (Y, curY) along a chain ΩY, read through
ιY, and the rounds on (X, cur) along Ω, read through ι, agree up to empty blow-ups when
curY is the pull-back of cur along a local analytic isomorphism g : Y → X carrying each ΩY k
into Ω k, and the two reading manifolds are identified by a local analytic isomorphism e over
g (eraseEmpty_resolveFrom_congr). This is the behaviour of a blow-up sequence functor under
smooth morphisms [Kol07, 34.1], the value on a pull-back being the pulled-back value with the empty
blow-ups deleted; in Włodarczyk's form, the restriction of the sequence over a larger open
determines the sequence over a smaller one [Wlo09, Theorem 2.0.3 (4)]. Its special cases carry the
canonicity proof of Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean: g = id with ΩY k ≤ Ω k
shrinks the chain, g an open inclusion restricts the outer open.
Per round, the field commutesWithLocalIsos of BOanFam, applied to the corestriction
g|_{ΩY d} : ΩY d → g(ΩY d), surjective onto its open relatively compact image (the first clause of
[Kol07, 34.1]), and the field compat along g(ΩY d) ≤ Ω d make the round on Y the erased
pull-back of the round on X along g|. So the derived manifolds are identified only through the
common erased list (eraseEmptyTransport: eraseEmptyLast on both sides and the cast stageOfEq),
the derived ideals correspond (markedTransformSeq_last_eraseEmptyTransport,
markedTransformSeq_last_pullbackLiftLast), and the derived boundary on Y is an empty subfamily
of the transported derived boundary on X (exists_orderEmbedding_eraseEmptyTransport, from
boundaryCorr_eraseEmpty), whose empty members resolveFrom_indiff
(Hironaka/Resolution/Analytic/Wlo09/Indiff.lean) removes before the induction hypothesis applies
to the exact pull-back (curX').pullback g'. The reading maps on the derived manifolds are
identified by uniqueness of maps over the blow-down (eq_of_stageMap_last_eq), and the two
concatenations are compared by eraseEmpty_concat_congr. The induction unfolds resolveFrom at the
successor case only.
BlowUpSequence.eraseEmptyTransport,stageMap_last_eraseEmptyTransport,stageMap_last_toAnalyticMap_eraseEmptyTransport,eraseEmptyTransport_apply: the identification of the last stages of two lists with the same erasure, over the base.BlowUpSequence.eq_of_stageMap_last_eq,BlowUpSequence.comap_comap_symm: uniqueness of maps over the blow-down (not in the sources: the blow-down is an isomorphism over a dense open, so two maps into the last stage that agree after it agree), the inverse-image identity along a diffeomorphism.BlowUpSequence.markedTransformSeq_last_eraseEmptyTransport,BlowUpSequence.exists_orderEmbedding_eraseEmptyTransport: the transport of the derived ideal and the derived boundary ([Kol07, 32 and 34.1]).BlowUpSequence.eraseEmpty_concat_congr: the two erased concatenations.mem_liftChain_iff: membership in the lifted chain.eraseEmpty_resolveFrom_congr: the transport theorem.
The identification of the last stages of two lists with the same erasure #
Two lists with the same deletion of empty blow-ups have isomorphic last stages ([Kol07, 34.1]):
through the common erased list, along eraseEmptyLast on both sides and the cast stageOfEq of
the equality of erasures.
Equations
Instances For
The identification lies over the identity of the base: the blow-downs agree.
The inverse image along a diffeomorphism then along its inverse is the identity
(comap_symm_comap the other way round).
stageMap_last_eraseEmptyTransport for the identification as an analytic map.
Uniqueness of maps over the blow-down (eq_of_stageMap_last_comp_eq; not in the sources):
a local analytic isomorphism and an analytic map into the last stage of a list that agree after
the blow-down agree, since the blow-down is an isomorphism over a dense open.
The marked transform at the last stage is transported along eraseEmptyTransport
([Kol07, 34.1]): both lists are the common erased list up to empty blow-ups, which transform
(I, m) by pull-back (markedTransformSeq_last_eraseEmpty).
For a list A without empty centres and a list B with the same erasure, the boundary family
from F at the last stage of A embeds order-preservingly into that of B transported along
eraseEmptyTransport, the members matched and the members of B's family off the range empty
(boundaryCorr_eraseEmpty_self); read on any family equal to B's. The empty blow-ups add empty
members to the boundary ([Kol07, 32 and 34.1]).
Deleting the empty blow-ups of two concatenations whose first pieces have the same erasure
(eraseEmptyTransport identifies their last stages) and whose second pieces agree up to empty
blow-ups after that identification gives equal lists (eraseEmpty_concat,
concat_pullback_stageOfEq).
Membership in the lifted chain: the point lies over the open of X.
Transport of the rounds along a local analytic isomorphism ([Kol07, 34.1];
[Wlo09, Theorem 2.0.3 (4)]). The rounds on (Y, curY) along a chain ΩY, read through ιY, and
the rounds on (X, cur) along Ω, read through ι, agree up to empty blow-ups when curY is
the pull-back of cur along a local analytic isomorphism g : Y → X carrying each ΩY k into
Ω k, and the two reading manifolds are identified by a local analytic isomorphism e over g
(ι ∘ e = g ∘ ιY). Per round: the field commutesWithLocalIsos along g|_{ΩY d} and compat
along g(ΩY d) ≤ Ω d (eraseEmpty_pullback_eraseEmpty, pullback_comp), then
eraseEmpty_concat and the induction hypothesis at the derived triples, identified through
markedTransformSeq_last_pullbackLiftLast and markedTransformSeq_last_eraseEmptyTransport (the
ideal), exists_orderEmbedding_eraseEmptyTransport (the boundary), resolveFrom_indiff and
resolveFrom_congr_triple, with the lifts of g and e.