Transport of the data of a blow-up sequence along an open immersion, without dimension #
Hironaka's Main Theorems II and II(N) and their Corollaries 1 and 3 [Hir64, pp. 142–146, 176] are
stated for a non-singular algebraic scheme, whose irreducible components may have different
dimensions, while the order reduction of the library runs on a scheme smooth of a single relative
dimension. The general case is assembled from the components: a succession on a component, an open
and closed subscheme U ⊆ X, is extended to X by the unit ideal on the complement
(Hironaka/Resolution/Algebraic/Hir64/ExtendOpen.lean), and the clauses are read off the pieces.
The transport lemmas of Hironaka/Scheme/BlowUpSequence/OpenTransport.lean do this for the weak
transforms when the ambient scheme is smooth of one relative dimension; this module proves the
transports needed with no smoothness hypothesis at all, for an open immersion u : Y ⟶ X and the
stage lifts u_i of the pull-back S.pullback u:
- the weak transform commutes with the pull-back along
uwhen the centre lies inside the range ofu(weakTransform_comap_blowUpMap_of_subset: the exceptional orders on the two sides agree, since the exceptional ideal is the unit ideal off the centre and divisibility by a power of an invertible ideal sheaf is containment, checked on stalks; the colon commutes with the inverse image along an open immersion of a locally Noetherian scheme), and also when the pulled-back centre is empty (weakTransform_comap_blowUpMap_of_comap_eq_top: both sides are the total transform);weakTransformSeq_pullback_mkiterates this along a sequence each of whose centres is inside or outside the range of the stage lift; - the reduced transform, a vanishing ideal, commutes with every open pull-back
(
reducedTransform_comap_blowUpMap, fromvanishingIdeal_comap_of_isOpenImmersion), hence so do Hironaka's boundariesE_i(boundarySeq_pullback_mk); - over an open
WofXmissing the image of every centre, each stage map restricts to an isomorphism (isIso_stageMap_restrict), and the weak transforms and boundaries are the inverse images of the initial data along the stage maps (weakTransformSeq_comap_ι_preimage,boundarySeq_comap_ι_preimage); over such an open the data is unchanged, the observation Hironaka makes in the proof of Corollary 1 [Hir64, p. 144]; - Hironaka's Definition 2 [Hir64, Ch. 0, §5, Definition 2] and the regularity of a point ascend
along an open immersion (
isSncBoundaryWith_of_comap_of_isOpenImmersion,exists_isRegularSystemOfParameters_apply_of_comap,isRegularAt_apply_iff_of_isOpenImmersion), the converse of the descent lemmas ofHironaka/Resolution/Algebraic/Hir64/ComponentDeletion.lean.
Inverse images along an open immersion #
The inverse image of a vanishing ideal sheaf along an open immersion is the vanishing ideal sheaf of the preimage: both are radical with that support.
The radical commutes with the inverse image along an open immersion.
The morphism of blow-ups over an open immersion is an open immersion (the square is cartesian).
The weak transform along an open pull-back #
The inverse image of the exceptional ideal along the morphism of blow-ups over u is the
exceptional ideal of the pulled-back centre.
The total transform of J pulled back along the morphism of blow-ups over u is the total
transform of u⁻¹ J.
If the pulled-back centre is empty, the weak transform along the blow-up pulls back to the weak transform of the pulled-back ideal: on both sides the exceptional ideal is the unit ideal, so both are the total transform.
If the centre lies inside the range of u, the exceptional orders of J along the blow-up of
D and of u⁻¹ J along the blow-up of u⁻¹ D agree: divisibility by a power of the invertible
exceptional ideal is containment, which holds off the centre (where the exceptional ideal is the
unit ideal) and over the range of u exactly when it holds on the pull-back.
If the centre lies inside the range of u, the weak transform along the blow-up pulls back to
the weak transform of the pulled-back ideal along the pulled-back centre: the exceptional orders
agree (exceptionalOrderAlong_comap_of_subset) and the colon commutes with the inverse image along
the open immersion of blow-ups.
The reduced transform red(π⁻¹(E) ∪ π⁻¹(D)) [Hir64, Main Theorem II (iii)] commutes with the
pull-back along an open immersion: it is the vanishing ideal sheaf of a closed set, and the
morphism of blow-ups over u is an open immersion under which the closed set pulls back to the
corresponding closed set of the blow-up of u⁻¹ D.
Along a pulled-back sequence #
Hironaka's boundaries of S.pullback u are the inverse images of the boundaries of S under
the stage lifts (reducedTransform_comap_blowUpMap stage by stage).
The weak transforms of S.pullback u are the inverse images of the weak transforms of S
under the stage lifts, provided every centre of S lies inside the range of its stage lift or
pulls back to the empty centre (weakTransform_comap_blowUpMap_of_subset,
weakTransform_comap_blowUpMap_of_comap_eq_top stage by stage).
weakTransformSeq_pullback_mk when every centre lies inside the range of its stage lift.
boundarySeq_pullback_mk in the Fin form.
Over an open missing the centres #
The blow-up map is an isomorphism over an open W on which the centre is the unit ideal
(blowUp.isIso_π_restrict_compl_support for a smaller open): the lift of W.ι inverts
π ∣_ W.
Over an open W missing the image of every centre, every stage map of the succession is an
isomorphism: each blow-up map is one over the preimage of W, and the restriction of a composite
is the composite of the restrictions (morphismRestrict_comp).
The inclusion of the preimage of W followed by the blow-up map is an open immersion when the
centre is the unit ideal on W: it is the isomorphism π ∣_ W followed by the inclusion of
W.
Over an open W on which the centre is the unit ideal, the weak transform is the inverse image
of the ideal: the exceptional ideal is the unit ideal there, so the colon by its powers changes
nothing.
Over an open W on which the centre is the unit ideal, the reduced transform of a reduced
E is the inverse image of E: the preimage of the centre is empty there, and the vanishing ideal
of the support of the reduced inverse image is that inverse image.
Over an open W missing the image of every centre, the weak transforms along the succession
are the inverse images of the ideal along the stage maps (weakTransform_comap_ι_preimage stage by
stage).
Over an open W missing the image of every centre, Hironaka's boundaries along the succession
are the inverse images of the reduced E₀ along the stage maps (reducedTransform_comap_ι_preimage
stage by stage).
Over an open W missing the image of every centre, the inclusion of the preimage of W
followed by the stage map is an open immersion (the isomorphism stageMap ∣_ W followed by the
inclusion of W).
Definition 2 and regularity ascend along an open immersion #
Hironaka's Definition 2 at a point u y in the range of an open immersion, from Definition 2
at y for the inverse images: the coordinates at y are carried to u y by the inverse of the
stalk isomorphism, the minimal primes and the generators with them (the converse of
IsSncBoundaryWith.comap_of_isOpenImmersion).
Definition 2 ascends along an open immersion whose range contains the support of D: E has
only normal crossings with D if u⁻¹ E has only normal crossings with u⁻¹ D.
A point in the range of an open immersion is regular iff its preimage is (the stalks are isomorphic).
Regularity at a point of a closed subscheme V(Z) in the range of the open immersion
V(Z.comap u) → V(Z) (a point over the range of u) is regularity at its preimage.