The centers of an order-m blow-up sequence lie over the cosupport #
For a smooth blow-up sequence S = (X_r → ⋯ → X_0 = X) of order m starting with (X, I)
([Kol07, Definition 66], IsOrderSeq), cosupp(I_{i+1}, m) ⊆ π_i^{-1}(cosupp(I_i, m)), hence
Π_i(Z_i) ⊆ cosupp(I, m) for every center Z_i. Consequently, for a flat ψ : U ⟶ X whose image
contains cosupp(I, m), every center lies in the image of the corresponding stage lift of ψ
(CentersInRange), no center of ψ^*S is empty when none of S is, and ψ^*S determines S
(pullback_injective). This is what allows étale equivalence [Kol07, Definition 96] and the
equality of étale equivalent blow-up sequences [Kol07, Theorem 97] to be used with étale maps
whose image contains the cosupport in place of étale surjections: the lifts of ψ still cover the
centers, so no empty
blow-up has to be deleted.
The one-blow-up step (le_ord_blowUpπ_of_le_ord_weakTransform). Let π : B_Z X → X be the
blow-up of a center Z along which ord I = m (condition (4) of Definition 66 at one stage), and
let y ∈ B_Z X with ord_y I' ≥ m for the weak transform I' = π_*^{-1} I. If π(y) ∈ Z then
ord_{π(y)} I ≥ m because ord_Z I = m means ord = m at the generic points of Z, and the
order is upper semicontinuous (leOrdAlong_iff_forall_mem, on the smooth X in characteristic
zero). If π(y) ∉ Z then π is an isomorphism near y and I' contains π^* I, so
ord_y I' ≤ ord_{π(y)} I (ord_controlledTransform_le_of_notMem; this is the part of
[Kol07, Lemma 61] concerning points off the exceptional divisor). The stage step and
Π_i(Z_i) ⊆ cosupp(I, m) follow by induction along the sequence, the stages being smooth of the
same relative dimension (smoothOfRelativeDimension_blowUpπ_comp_of_smooth).
One blow-up: if ord_Z I = m along the center Z and y ∈ B_Z X has ord_y π_*^{-1} I ≥ m,
then ord_{π(y)} I ≥ m; over the center by upper semicontinuity of the order, off it because π
is an isomorphism there and π_*^{-1} I ⊇ π^* I (ord_controlledTransform_le_of_notMem; compare
[Kol07, Lemma 61]).
The stage step: for a smooth blow-up sequence S of order m starting with (X, I),
cosupp(I_{i+1}, m) ⊆ π_i^{-1}(cosupp(I_i, m)); induction along the sequence with
le_ord_blowUpπ_of_le_ord_weakTransform at the first step (on the cons shape the first step is
D.blowUpπ once the tail's constructor is known, step_cons_nil_zero, step_cons_cons_zero).
Every center of a smooth blow-up sequence of order m starting with (X, I) lies over the
cosupport, Π_i(Z_i) ⊆ cosupp(I, m): by induction along the sequence, a point of Z_i has
ord I_i ≥ m (condition (4) of [Kol07, Definition 66] with upper semicontinuity), and
le_ord_blowUpπ_of_le_ord_weakTransform carries ord ≥ m down each blow-up.
For a flat ψ : U ⟶ X whose image contains cosupp(I, m), the centers of a smooth blow-up
sequence of order m starting with (X, I) lie in the images of the stage lifts of ψ
(CentersInRange): Z_i ⊆ Π_i^{-1}(cosupp(I, m)) ⊆ Π_i^{-1}(im ψ) = im ψ_i
(range_pullbackStageHom).
If no center of S is empty and every center lies in the image of the corresponding stage
lift of ψ, then no center of ψ^*S is empty: by induction along the sequence; at each stage the
pulled-back center is ψ_i^{-1}(Z_i), whose support is the preimage of the nonempty
|Z_i| ⊆ im ψ_i (support_comap, support_eq_bot_iff).
ψ^*B determines B when the image of ψ contains the cosupport (a closed subscheme
contained in the image of an étale map is determined by its preimage): two smooth blow-up
sequences of order m starting with (X, I) with equal pullbacks along a flat ψ whose image
contains cosupp(I, m) are equal (pullback_injective with centersInRange_of_cosupp_le_range;
compare the uniqueness for surjective h in [Kol07, 30.1]).