BED commutes with smooth surjections #
Clause (d) of [Wlo05, Theorem 1.0.2] ([Wlo05, 4.1]; the first bullet of [Kol07, 34.1]): for a
smooth surjection h : X' → X carrying the pull-back data,
BED(X', h^* I_Y, ∅) = h^* BED(X, I_Y, ∅) (bed_pullback_of_surjective), where BED is the loop
of Hironaka.Resolution.Algebraic.Wlo05.Embedded.
The mechanism (the proof of [Wlo05, Theorem 4.7.1] transported along h): the loop bedAux is
a recursion on the number of remaining components, and one round is transported as follows.
- The runs:
BMO_1commutes with smooth surjections ([Kol07, Theorem 69 (2)],dimFreeBMO_commutesWithSmoothofHironaka.Resolution.Algebraic.Stage.DimFreeTheorems), so the pulled-back run is the pull-back of the run ([Kol07, Definition 30, 30.1]). - The stop rule: with
C'the components of the preimages of the members ofC(IsPullbackComponents,Hironaka.Resolution.Algebraic.Wlo05.EmbeddedPullbackTools), the first absorbing stage is the same on both sides and the same components are absorbed (stopRule_aux), soNat.findagrees. - The isolated triple: the marked triple induced at the end of the truncation pulls back along the
last-stage lift (
isPullbackOf_induced_last), and its colon divisor — the reduced ideal of the union of the absorbed strict transforms — pulls back too: the colon commutes with a flat base change (colon_comap_of_flat_of_isLocallyNoetherian,Hironaka.Scheme.BlowUp.FlatColon), the reduced ideal of a closed set pulls back to the reduced ideal of the preimage (comap_vanishingIdeal_of_smooth,Hironaka.Resolution.Algebraic.Smooth.GeometricallyReduced), and the preimage of the union of the absorbed strict transforms is the union of the strict transforms of the absorbed components upstairs (iSup_support_strictTransformSeq_pullback_last: the strict transform of a finite union is the union of the strict transforms). - The remaining components: the strict transforms of the components of
h⁻¹(V(c))are the components ofh_n⁻¹(X̄_n(c))(isPullbackComponents_remainingAt, through the generic points of the strict transforms, the proof of [Kol07, Corollary 22]), so the invariantIsPullbackComponentsholds again along the last-stage lift, and strong induction onC.cardcloses.
The isolated triple and the remaining members are isolatedAt and remainingAt of
Hironaka.Resolution.Algebraic.Wlo05.Embedded at the truncated run and the absorbed family; stating
the transport for these, with the run and the families as parameters, is what lets the pulled-back
run be substituted (concat_bedAux_congr). This transport is not in the literature.
Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedEraseEmpty and
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses.
The round with the run as a parameter #
Substitution of the run and of the absorbed and remaining families in the concatenation of a round (the form of the loop on the left, the parametrised form on the right).
The loop unrolled once at the first absorbing stage n, for any n equal to Nat.find.
The isolated triple pulls back along the last-stage lift #
The isolated marked triple of the pulled-back truncated run, with the absorbed family F',
carries the pull-back data of the isolated marked triple downstairs along a lift g of the last
stages ([Wlo05, 4.1] for the isolated triple), given that the induced triples do
(isPullbackOf_induced_last for the last-stage lift) and that 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) and the reduced ideal of a closed set pulls back to the reduced
ideal of the preimage (Hironaka.Resolution.Algebraic.Smooth.GeometricallyReduced). Stated for a
lift g typed at the stages stage (Fin.last _), to which last unfolds only definitionally.
The set underlying a finite supremum of closed sets.
The strict transform at the end of the pulled-back run of the preimage of V(c) is the union
of the strict transforms of the components of h⁻¹(V(c)).
The union of the strict transforms of the components of the preimages of the members of F is
the preimage, under a lift g of the last stages carrying the strict transforms
([Kol07, Definition 30, 30.2]; strictTransformSeq_pullback_last for the last-stage lift), of the
union of the strict transforms of the members of F ([Wlo05, 4.1] for the divisor of the isolated
triple).
The remaining members pull back as components #
For the state (C, C') of the loop and the predicates P, P' selecting the non-absorbed
members (related through the stop-rule equivalence), the strict transforms at the end of the
pulled-back run of the members of C'.filter P' are the components of the preimages, under a lift
g of the last stages, of the strict transforms of the members of C.filter P (the proof of
[Kol07, Corollary 22] and [Kol07, Definition 30, 30.2] along h), given that no member was
absorbed along the truncated run on either side, that g carries the strict transforms (hg) and
the generic points (hgen; both hold for the last-stage lift).
The remaining members at the end of a truncated run along which no member was absorbed are
reduced ideals of closures of points (integral strict transforms,
exists_isGenericPoint_strictTransformSeq).
The loop along a smooth surjection #
The loop along a smooth surjection ([Wlo05, Theorem 1.0.2] clause (d), [Wlo05, 4.1]; the
first bullet of [Kol07, 34.1]): for marked triples of mark 1, a smooth surjection h carrying the
pull-back data, a family C of reduced ideals of irreducible closed sets and C' the components
of their preimages, the modified run upstairs is the pull-back of the modified run downstairs.
Strong induction on the number of members; one round is transported by the stop-rule equivalence,
the pull-back data of the isolated triple and the components relation for the remaining
members.
BED commutes with smooth surjections ([Wlo05, Theorem 1.0.2] clause (d), [Wlo05, 4.1];
the first bullet of [Kol07, 34.1]): for a smooth surjection h : X' → X carrying the pull-back
data, BED(X', h^* I_Y, ∅) = h^* BED(X, I_Y, ∅) — the loop bedAux_pullback_of_surjective on the
components of V(I_Y) and of V(h^* I_Y) (isPullbackComponents_componentIdeals). 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).