Transport of the order conditions to the componentwise sequence #
If ord_{Z_k} J = d for every component Z_k of a smooth center Z = ∐ Z_k, the componentwise
sequence is again a smooth blow-up sequence of order d [Kol07, Definition 66]: the intermediate
centers Z_k' are smooth with ord = d and have simple normal crossings with the running total
transform, because the earlier blow-ups are isomorphisms near Z_k'. The proof here makes that
local statement global by the device of [Kol07, Proposition 37]: Definition 66 is local on X
(isOrderSeq_of_covers, Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Local.lean), so cover
X by the opens
U_k := X ∖ ⋃_{l ≠ k} Z_l (one for each component) and U_∞ := X ∖ Z.
Over U_k every center but Z_k is empty and Z ∩ U_k = Z_k ∩ U_k, so the pulled-back sequence is
a single smooth blow-up of order d of (U_k, J|_{U_k}, E|_{U_k}) preceded and followed by empty
blow-ups [Kol07, Warning 20]; over U_∞ every blow-up is empty. The pullback of ofCenters c D
along an open immersion is ofCenters of the inverse images (pullback_ofCenters), a sequence all
of whose centers are empty is of order d for any triple (isOrderSeq_ofCenters_top), and a
sequence with one non-empty center carrying the conditions of Definition 66 is of order d
(isOrderSeq_ofCenters_of_single: the empty blow-ups are isomorphisms along which the pullback
transport of Hironaka/Sequence/Pullback*.lean carries the conditions, the total transform
gaining only empty components, ExtendsByEmpty). Descent along the cover is
isOrderSeq_of_covers.
Main declarations #
hasSncWith_top,ordAlongEq_top,ExtendsByEmpty.hasSncWith_of,extendsByEmpty_comap_totalTransform_top: the empty-center bookkeeping.AlgebraicGeometry.Scheme.BlowUpSequence.pullback_ofCenters: pullbacks of componentwise sequences.isOrderSeq_ofCenters_top,isOrderSeq_ofCenters_of_single,isOrderSeq_ofCenters(the order condition for the componentwise sequence).isIso_subschemeMap_center_ofCenters,irreducibleSpace_center_ofCenters,isRegular_center_ofCenters: the intermediate centers are isomorphic to the components.
The pullback [Kol07, 30.1] of the componentwise sequence of D 0, …, D (c-1) along h is the
componentwise sequence of the inverse images h⁻¹ D i: the squares of blowUpMap (blowUpMap_π)
carry each pulled-back center across the earlier blow-ups.
Empty centers: the empty blow-up of Warning 20 satisfies Definition 66 vacuously #
The unit ideal sheaf (the empty center) has simple normal crossings with every family: there is no point to check.
Every ideal sheaf has order m along the empty center: there is no generic point to check.
Simple normal crossings with a closed subscheme extend along an extension by empty components
(the converse of ExtendsByEmpty.hasSncWith): a component of the extended family through a point
is a component of the original family through it.
The total transform of E under the empty blow-up is E pulled back along the (isomorphic)
blow-up map, extended by the empty exceptional component ([Kol07, Warning 20];
extendsByEmpty_totalTransform_top_comap_inv read on the blow-up).
Sequences with at most one non-empty center #
A componentwise sequence all of whose centers are empty is a smooth blow-up sequence of order
d for every triple ([Kol07, Warning 20 and 32]: empty blow-ups may be interspersed freely).
A componentwise sequence with a single non-empty center D k₀, which is smooth over k, has
order d for J and has simple normal crossings with E, is a smooth blow-up sequence of order
d for (X, J, E): the empty blow-ups before D k₀ are isomorphisms [Kol07, Warning 20] along
which the pullback transport carries the conditions (smooth_subschemeι_comap_comp,
ordAlongEq_comap_of_smooth, hasSncWith_comap_of_smooth), the weak transform along an empty
blow-up being the inverse image (weakTransform_top_left) and the total transform the inverse
image extended by an empty component; the empty blow-ups after it satisfy Definition 66
vacuously.
The componentwise sequence of a disjoint union is of order d #
The inverse image of a center along the inclusion of an open set missing its support is the unit ideal sheaf.
If the disjoint union Z = ∏ i, D i of the pairwise disjoint centers D i is smooth over k,
has order d along each D i and has simple normal crossings with E, then the componentwise
sequence is a smooth blow-up sequence of order d for (X, J, E) [Kol07, Definition 66]. Proof:
Definition 66 is local on X (isOrderSeq_of_covers); on the open U_k = X ∖ ⋃_{l ≠ k} V(D l)
the sequence pulls back (pullback_ofCenters) to a single blow-up of Z ∩ U_k = V(D k) ∩ U_k
among empty ones (isOrderSeq_ofCenters_of_single), and on U_∞ = X ∖ V(Z) to empty blow-ups
(isOrderSeq_ofCenters_top); the conditions on Z restrict to the pieces by the pullback
transport along the open immersions.
The intermediate centers are isomorphic to the components #
The open U_{k₀} = X ∖ ⋃_{l ≠ k₀} V(D l): away from every center but D k₀.
Equations
- Hironaka.Sequence.complOthers D k₀ = ((Finset.univ.erase k₀).sup fun (l : Fin c) => (D l).support).compl
Instances For
When the first i centers of a blow-up sequence are empty, the partial composite Π_i is an
isomorphism (a composite of the isomorphisms π_∅, [Kol07, Warning 20]).
For pairwise disjoint centers, the morphism V(Z_k') → V(D k), the base change of Π_k along
V(D k) → X, is an isomorphism (the intermediate center Z_k' is the isomorphic preimage of
Z_k, the earlier blow-ups being isomorphisms near it): over U_k = X ∖ ⋃_{l ≠ k} V(D l), which
contains V(D k), the earlier blow-ups are empty, so the base change of Π_k along U_k → X
(isPullback_pullbackStageHom) is a composite of the isomorphisms of [Kol07, Warning 20].
For pairwise disjoint irreducible centers, every center of the componentwise sequence is
irreducible: V(Z_k') ≅ V(D k) (isIso_subschemeMap_center_ofCenters).
For pairwise disjoint regular centers, every center of the componentwise sequence is regular:
the stalks correspond under the isomorphism V(Z_k') ≅ V(D k)
(IsRegularLocalRing.of_ringEquiv).