The last-stage transforms along the deletion of empty blow-ups #
Deleting the empty blow-ups of a list L ([Kol07, 34.1], BlowUpSequence.eraseEmpty) identifies
the
last stages along BlowUpSequence.eraseEmptyLast
(Hironaka.Resolution.Analytic.Functor.EraseEmptyConcat). This file transports the last-stage
data along that identification: the weak transform, the marked transform (for a list whose
markings are legitimate) and the strict transform at the last stage of the cleaned list are the
pull-backs along eraseEmptyLast⁻¹ of those of the list (weakTransformSeq_last_eraseEmpty,
markedTransformSeq_last_eraseEmpty, strictTransformSeq_last_eraseEmpty; the counterparts for
schemes are in Hironaka.Resolution.Algebraic.Kol07.EraseEmptyInduced).
The proofs are by recursion on the list. A kept step contributes the same transform on both
sides (cons_*Aux_succ). A deleted step contributes, on the list's side, the transform along an
empty blowing-up: the exceptional ideal sheaf is the unit ideal sheaf, so the marked and weak
transforms are the total transform (birationalTransform_I_of_eq_empty,
weakTransformOf_of_eq_empty), and the strict transform of a closed set is its preimage
(strictTransformSet_empty_of_isClosed); on the cleaned list's side it contributes the transport
of the cleaned tail along the isomorphism Bl_∅ M ≃ M, i.e. along BlowUpSequence.map. The
transports along map (*_last_map) are themselves by recursion, each step the naturality of the
one-step transform along the lift liftDiffeomorph of the isomorphism, obtained from the
naturalities along liftStep (Hironaka.Resolution.Analytic.Functor.PullbackTransport) by the
uniqueness of lifts (*_of_square).
The marked transport needs the markings to be legitimate along the list, i.e. the order clause
of [Kol07, Definition 66] alone (FiniteSuccession.IsMarkedGe, implied by IsOfOrderGe); its
normal-crossings clause plays no role, so the marked transport is stated for any IsOfOrderGe
boundary.
The transforms along an empty blowing-up #
The ideal sheaf of the empty submanifold is the unit ideal sheaf.
Division by the unit ideal sheaf changes nothing: the colon by ⊤ ^ m is the ideal itself.
Kollár (60.1) along an empty blowing-up: the exceptional ideal sheaf is the unit ideal sheaf, so the marked transform is the total transform.
Hironaka's weak transform [Hir64, Ch. 0, §5, p. 142] along an empty blowing-up: the weak transform is the total transform.
The strict transform of a closed set under a blowing-up along the empty centre is its preimage (the closure of the preimage of the complement of the centre, here everything).
The bundled weak transform along the chosen blowing-up of an empty centre is the pull-back.
Kollár (60.1) along the chosen blowing-up of an empty centre: the marked transform is the pull-back.
The analytic isomorphism Bl_∅ M ≃ M of an empty blowing-up, as an analytic map, is the
blow-down (emptyBlowUpDiffeomorph_apply, bundled).
Naturality of the one-step transforms along a lift over a local analytic isomorphism #
weakTransform_comap_liftStep for any analytic map G between the chosen blowings-up lying
over h with S = h⁻¹(Y): such a G is the lift liftStep (uniqueness of lifts,
heq_liftStep_of_forall).
birationalTransform_comap_liftStep for any G over h with S = h⁻¹(Y).
The strict transform (the closure of the preimage of the complement of the centre) is natural
along a local analytic isomorphism G between blowings-up lying over h with S = h⁻¹(Y):
G⁻¹(closure π⁻¹(H ∖ Y)) = closure π'⁻¹(h⁻¹(H) ∖ h⁻¹(Y)), the preimage of a closure under an open
continuous map being the closure of the preimage.
The total transform of a hypersurface family is natural along a local analytic
isomorphism G between blowings-up lying over h with S = h⁻¹(Y): the strict transforms by
strictTransformSet_preimage_of_square, the exceptional divisor over h.
Transport along a diffeomorphism and its lift #
The lift of φ : M ≃ N to the blowings-up lies over φ (blowDown_liftPoint).
The ideal sheaf of the transported centre φ(Y) pulls back to the ideal sheaf of Y.
The order along the transported centre φ(Y) at φ a is the order along Y of the pulled-back
ideal sheaf at a (ordAlongIdeal_comap_of_isLocalDiffeomorphAt).
The order clause of [Kol07, Definition 66] alone #
Clause (4′) of [Kol07, Definition 66] alone: the marked transform of (I, m)
has order ≥ m along every centre, so that every marked transform along the sequence is Kollár's
(60.1) (the marking legitimate). IsOfOrderGe is this clause together with the
normal-crossings clause (3′) (IsOfOrderGe.isMarkedGe).
Equations
- S.IsMarkedGe I m = ∀ (i : Fin S.length), ∀ a ∈ Manifold.IdealSheaf.support (S.center i), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal (S.center i) (S.markedTransformSeq I m i.castSucc) a
Instances For
The constructor form of IsMarkedGe (the order clause of isOfOrderGe_cons_iff).
The marked transform at the last stage of cons ψ₀ hY rest is the marked transform along
rest of the marked transform of the first step (cons_markedTransformSeqAux_succ with
cons_markedTransformSeq_one).
Along an empty first step the marked transform is the pull-back.
Transport of the last-stage data along map #
The first marked transform along the transported list pulls back, along the lift of
φ, to the first marked transform along the list (birationalTransform_comap_of_square at the
first step).
The marking stays legitimate along the transport of a list: (φ^{-1})^* of a marking legitimate
for φ^* I is legitimate for I.
The weak transform at the last stage of the transported list Z.map φ is the pull-back along
(mapLast φ)⁻¹ of the weak transform of φ^* J at the last stage of Z
(weakTransform_comap_of_square at each step).
The marked transform at the last stage of the transported list Z.map φ, for a legitimate
marking, is the pull-back along (mapLast φ)⁻¹ of the marked transform of φ^* I at the last
stage of Z (birationalTransform_comap_of_square at each step).
The strict transform at the last stage of the transported list Z.map φ is the preimage under
(mapLast φ)⁻¹ of the strict transform of φ⁻¹(H) at the last stage of Z
(strictTransformSet_preimage_of_square at each step).
Transport along an equality of lists #
The last-stage transforms along the deletion of empty blow-ups #
[Kol07, 34.1]: deleting the empty blow-ups keeps the markings legitimate — an
empty step is a legitimate marking vacuously and transforms (I, m) by pull-back.
[Kol07, 34.1], the analogue of weakTransformSeq_eraseEmpty_last for schemes: the
weak transform of I at the last stage of the cleaned list is the pull-back along
eraseEmptyLast⁻¹ of the weak transform at the last stage of the list — a kept step contributes
the same weak transform on both sides, a deleted step the total transform along the empty
blowing-up, which the transport of the cleaned tail along Bl_∅ M ≃ M absorbs.
The marked version of weakTransformSeq_last_eraseEmpty, for a list whose markings are
legitimate (markedTransformSeq_eraseEmpty_last).
[Kol07, 34.1], the analogue of markedTransformSeq_eraseEmpty_last for schemes: for a
list of order ≥ m for (I, m, E₀) ([Kol07, Definition 66], any boundary E₀), the marked
transform of (I, m) at the last stage of the cleaned list is the pull-back along
eraseEmptyLast⁻¹ of the marked transform at the last stage of the list (only the order clause
is used: markedTransformSeq_last_eraseEmpty_of_isMarkedGe).
[Kol07, 34.1], the analogue of strictTransformSeq_eraseEmpty_last for schemes: the
strict transform of a closed set H at the last stage of the cleaned list is the preimage under
eraseEmptyLast⁻¹ of its strict transform at the last stage of the list — a deleted step
transforms a closed set by preimage (strictTransformSet_empty_of_isClosed). Closedness is
needed: the strict transform along an empty blowing-up of a non-closed set is the preimage of its
closure.