BED commutes with smooth morphisms up to empty blow-ups #
Clause (d) of [Wlo05, Theorem 1.0.2] ([Wlo05, 4.1]) and the second bullet of [Kol07, 34.1]
(Kollár's "deleting every blow-up h^* π_i whose center is empty") for the loop BED of
Hironaka.Resolution.Algebraic.Wlo05.Embedded, under the hypothesis that the image of the smooth h : X' → X meets every irreducible component of Y = V(I_Y): then BED(X', h^* I_Y, ∅) is the
pull-back h^* BED(X, I_Y, ∅) with its empty blow-ups deleted (bed_pullback_eraseEmpty).
The mechanism is the transport of the loop along a smooth surjection
(bedAux_pullback_of_surjective, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedPullback) with two
changes, both coming from Kollár's deletion of the empty blow-ups and the reindexing:
- the invariant of the loop is the pull-back relation UP TO UNIT BOUNDARY MEMBERS
(
MarkedTriple.IsPullbackOfUpToUnits,Hironaka.Resolution.Algebraic.MarkedOrderReduction.UpToUnits): the deleted empty blow-ups leave unit members in the boundary of the pulled-back data, so the isolated marked triple upstairs is the pull-back of the one downstairs only up to those members. The run ofBMO_1does not see them (dimFreeBMO_indifferentToEmptyMembers), so the second bullet of [Kol07, 34.1] forBMO_1([Kol07, Theorem 69 (2)]) gives the run upstairs as the ERASED pull-back of the run downstairs (bmoOneRun_eraseEmpty_pullback); - the stop rule is transported across
eraseEmptyby the reindexing ofHironaka.Resolution.Algebraic.Kol07.Thm36.EraseEmptyIndex: the stages of the erased run are the nonempty stages of the pulled-back run (exists_eraseIdx_eq), and an empty centre absorbs nothing alive — the first absorbing stage downstairs absorbs a component upstairs (the image hypothesishmeetsgives one), whose strict transform is nonempty, so the pulled-back centre there is nonempty and survives the erasure (centerContains_eraseEmpty_iff). Surjectivity ofhentered the surjective case only there (a component ofh⁻¹(V(c))exists) and in the identity of the runs.
The round is then assembled by pullback_concat, eraseEmpty_concat (the erasure of a
concatenation, the second piece carried along the last-stage isomorphism eraseEmptyLastHom) and
eraseEmpty_pullback_of_flat_surjective along that isomorphism; the isolated triple and the
remaining components are transported along eraseEmptyLastHom ≫ pullbackLastHom
(IsPullbackOfUpToUnits.induced_eraseEmpty, strictTransformSeq_eraseEmpty_last,
isPullbackComponents_comp, isPullbackComponents_image_comap_of_isIso), and the image hypothesis
propagates to the remaining components (the generic point of a component upstairs lies over the
strict transform downstairs). This transport is not in the literature. Used in
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses.
The run of BMO_1 on a pull-back up to unit members #
The second bullet of [Kol07, 34.1] for BMO_1 on a pull-back up to unit boundary members: the
run of BMO_1 on T' is the erased pull-back of the run on T — T' and its full pull-back have
the same run (dimFreeBMO_indifferentToEmptyMembers), and the full pull-back is an exact pull-back
(dimFreeBMO_commutesWithSmooth, [Kol07, Theorem 69 (2)]).
The pull-back of a run of order ≥ m is a run of order ≥ m for the pull-back data up to unit
members (the run of the full pull-back with the deleted members restored,
ExtendsByEmpty.isOrderGeSeq).
The erased pull-back of a run of order ≥ m is a run of order ≥ m for the pull-back data up
to unit members (IsOrderGeSeq.eraseEmpty).
Components of preimages along a composite and along an isomorphism #
The preimage of a closed set along a composite.
The components of the preimages compose ([Kol07, Definition 30, 30.1] twice): the components
of e⁻¹(V(b)), b a component of g⁻¹(V(c)), are the components of (e ≫ g)⁻¹(V(c))
(mem_genericPoints_preimage_iff for the open map e).
Along an isomorphism e, the components of the preimages of the members of B (reduced
ideals of closures of points) are their inverse images b.comap e.
The remaining members at the end of the erased run are the inverse images, along the
last-stage isomorphism, of the remaining members at the end of the run
(strictTransformSeq_eraseEmpty_last).
The isolated triple along the erased run #
isolatedAt_isPullbackOf up to unit members: the isolated marked triple of a run Q'
upstairs is the pull-back up to unit members of the isolated marked triple of Q downstairs along
a smooth lift g of the last stages, when the induced triples are and the union of the absorbed
strict transforms upstairs is the preimage of the one downstairs (the colon commutes with the flat
lift, Hironaka.Scheme.BlowUp.FlatColon; the reduced ideal of a closed set pulls back to the
reduced ideal of the preimage, Hironaka.Resolution.Algebraic.Smooth.GeometricallyReduced).
The union of the strict transforms at the end of the ERASED pulled-back run of the components
of the preimages of the members of F is the preimage, along eraseEmptyLastHom ≫ g, of the
union of the strict transforms of the members of F
(iSup_support_strictTransformSeq_pullback_last carried along the last-stage isomorphism,
strictTransformSeq_eraseEmpty_last).
The loop along a smooth morphism meeting every component #
The loop along a smooth morphism meeting every component ([Wlo05, Theorem 1.0.2] clause
(d), [Wlo05, 4.1]; the second bullet of [Kol07, 34.1]): for marked triples of mark 1, a smooth
h carrying the pull-back data up to unit boundary members, a family C of reduced ideals of
irreducible closed sets each meeting the image of h, and C' the components of their
preimages, the modified run upstairs is the pull-back of the modified run downstairs with its
empty blow-ups deleted. Strong induction on the number of members: one round is transported by
the stop-rule equivalence (stopRule_aux) read across the erasure
(centerContains_eraseEmpty_iff, exists_eraseIdx_eq_of_lt), the pull-back data up to unit
members of the isolated triple, the components relation for the remaining members and the image
hypothesis for them; the round is assembled by pullback_concat and eraseEmpty_concat.
BED commutes with smooth morphisms up to empty blow-ups ([Wlo05, Theorem 1.0.2] clause
(d); the second bullet of [Kol07, 34.1]): for a smooth h : X' → X carrying the pull-back data
whose image meets every irreducible component of Y (every specialization-maximal point η of
V(I_Y) has Set.range h ∩ closure {η} nonempty),
BED(X', h^* I_Y, ∅) = (h^* BED(X, I_Y, ∅)).eraseEmpty — the loop bedAux_eraseEmpty_pullback on
the components of V(I_Y) and of V(h^* I_Y) (isPullbackComponents_componentIdeals), the
generic points of the components being exactly the maximal points of the hypothesis. The
hypothesis hE is present because clause (d) of [Wlo05, Theorem 1.0.2] is stated for the
embedded desingularization of Y with empty boundary, the setting in which
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses applies this theorem; the proof does
not need it, because the transport of the loop works for any marked triple of mark 1 whose members
are the reduced ideals of the components (componentIdeals_prime).