The induced data of a blow-up sequence under a smooth pullback #
Along a smooth morphism h : Y → X the induced ideals and divisors of the pulled-back sequence are
the pullbacks of the induced ideals and divisors, and the order conditions of
[Kol07, Definition 66] are preserved ([Wlo05, Proposition 2.4.2]; [Kol07, 34.1]). This module
proves the identifications of the induced data; the transport of the order conditions is in
Hironaka/Scheme/BlowUpSequence/PullbackSnc.lean. Its pieces:
- the exceptional divisor of the pulled-back blow-up is the inverse image of the exceptional
divisor, for every
h(exceptionalDivisor_comap, the defining square ofblowUpMap); - nonvanishing on every component is preserved by flat pullback
(
isNonzeroEverywhere_comap_of_flat): the local homomorphisms of stalks of a flat morphism are faithfully flat, so a nonzero ideal extends to a nonzero ideal; - the marked transform
𝒪(mF) · π^* Iof [Kol07, Definition 60] commutes with base change along the morphism of blow-ups over anyh, in the domainF^m ∣ π^* Iof that definition (markedTransform_comap_blowUpMap_of_pow_dvd): the identityF^m · π_*^{-1}(I, m) = π^* Ipulls back,comapbeing multiplicative, and the uniquenesseq_markedTransform_of_pow_mul_eqidentifies the pullback with the marked transform of the pulled-back data; iterated along a sequence of order≥ mthis givesIsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom, the general form of [Kol07, Lemma 62]; - the strict and total transforms along the sequence commute with flat pullback
(
strictTransformSeq_pullback,totalTransformSeq_pullback), and the empty divisor family pulls back to the empty one (empty_comap); - the order along a center is preserved by smooth pullback (
ordAlongEq_comap_of_smooth,leOrdAlong_comap_of_smooth): a flat morphism is generalizing (Mathlib'sFlat.generalizingMap), so the generic points ofh⁻¹|Z|map to generic points of|Z|, whereord_comap_of_smoothreads the order; - along a smooth blow-up sequence of order
mthe weak transforms pull back (IsOrderSeq.weakTransformSeq_pullback): each weak transform is the marked transform with controlm, and the marked transform pulls back.
The statements come in two forms: with a relative dimension d of h, and with only the
equidimensionality of the source Y over k (suffix _of_equidim, _of_smooth), the form
available when the pulled-back triple is given.
The exceptional divisor and the marked transform under base change #
The exceptional divisor of the pulled-back blow-up is the inverse image of the exceptional
divisor under the morphism of blow-ups over h, for every h Wlo05, Proposition 2.4.2,
proof.
The marked transform 𝒪(mF) · π^* I commutes with base change along the morphism of blow-ups
over any h : Y ⟶ X, in the domain F^m ∣ π^* I of [Kol07, Definition 60]: the identity
F^m · π_*^{-1}(I, m) = π^* I pulls back along blowUpMap h D through the square blowUpMap_π,
and the quotient by the invertible F_Y^m is unique (eq_markedTransform_of_pow_mul_eq). This is
the general form of [Kol07, Lemma 62], which is the case of the closed immersion of a hypersurface
H ⊇ Z; the statement assumes no flatness of h and neither Z ⊊ H nor I|_H ≠ 0.
Nonvanishing and the order along a center under pullback #
Nonvanishing on every irreducible component ([Kol07, Notation 64 (2)]) is preserved by flat
pullback: the stalk map of a flat morphism is faithfully flat, so a nonzero ideal extends to a
nonzero ideal (comap_stalkMap_map_eq_self).
A flat morphism is generalizing [TSPA, Tag 01U1], so a generic point of the preimage h⁻¹|Z|
maps to a generic point of |Z|.
The order along a center is preserved by smooth pullback, ord_{Z ×_X Y}(h^* I) = ord_Z I
("ord_{x'}(I'_i) = ord_x(I_i)", [Wlo05, Proposition 2.4.2, proof]; ord_comap_of_smooth);
vacuous when the pulled-back center is empty.
The ≥ m form of ordAlongEq_comap_of_smooth.
The strict and total transforms under flat base change #
The colon by a principal ideal commutes with flat base change, (I : e) S = (I S : φ(e))
([Mat89, Theorem 7.4 (iii)], for a principal divisor). The inclusion
⊇ is the equational criterion for flatness [TSPA, Tag 00HK]: a relation
s · φ(e) = Σ_k c_k φ(i_k) with i_k ∈ I is trivial, s = Σ_j φ(a_j) y_j with
e a_j + Σ_k i_k a_{kj} = 0, so each a_j ∈ (I : e).
The colon by an invertible ideal sheaf commutes with flat base change: on stalks
(stalkIdeal_colon_of_isInvertible on both sides, IsInvertible.comap_of_flat) both sides are
the colon by the image φ(e) of a generator of the principal stalk, map_colon_singleton_of_flat
([Wlo05, Proposition 2.4.2, proof]).
The saturation ⋃ᵢ (J : Kⁱ) by an invertible K commutes with flat base change, termwise by
colon_comap_of_flat.
The strict transform of a closed subscheme commutes with flat base change along the morphism
of blow-ups over h ("E'_{i+1} = φ_{i+1}^{-1}(E_{i+1})", [Wlo05, Proposition 2.4.2, proof];
[Kol07, Definition 65]): the strict transform is the saturation of the total transform by the
exceptional divisor, the total transform pulls back along the square blowUpMap_π, the
exceptional divisor by exceptionalDivisor_comap.
The total transform of a divisor family [Kol07, Definition 65] commutes with flat base change: componentwise, strict transforms to strict transforms and the exceptional divisor to the exceptional divisor.
totalTransformSeq_pullback in the ⟨j, hj⟩ form of the indices: by induction on the
sequence, totalTransform_comap_of_flat at the head and the inductive hypothesis for the tail
along blowUpMap h D.
Along a flat pullback the induced divisor families of h^* B for h^{-1} E are the inverse
images of those of B for E under the stage lifts: "the divisors in E'_i are the inverse
images of the divisors in E_i" [Wlo05, Proposition 2.4.2 (2)].
The inverse image of the empty divisor family is the empty divisor family (used where the
divisorial part E of a triple is ignored, as in [Kol07, Definition 78]).
strictTransformSeq_pullback in the ⟨j, hj⟩ form of the indices: along a flat h the
strict transform of h⁻¹(Y) along the pulled-back sequence is the inverse image under the stage
lift of the strict transform of Y, by induction on the sequence, strictTransform_comap_of_flat
at the head and the inductive hypothesis for the tail along blowUpMap h D, exactly as
totalTransformSeq_pullback_mk.
Along a flat pullback the strict transform of the inverse image of a closed subscheme along the pulled-back sequence is the inverse image, under the stage lift, of its strict transform along the original sequence ([Kol07, 30.2 and 34.1]); used for the locality of maximal contact.
strictTransformSeq_pullback at the stage of the i-th center, indexed through
pullbackCenterIdx as center_pullback is (the two index transports agree definitionally).
The induced data of a smooth blow-up sequence under smooth pullback #
The weak transform commutes with base change along a smooth h whose source is
equidimensional over k (h ≫ f smooth of some relative dimension n'); no relative dimension
of h is needed, as the argument uses d only through d + n.
In the setting of [Kol07, Definition 66] (ambient scheme smooth and equidimensional over k
of characteristic zero, smooth center Z, ord_Z I = m along every component of Z) the weak
transform commutes with base change along the morphism of blow-ups over a smooth h
([Wlo05, Proposition 2.4.2, proof]; compare the birational transform of [Kol07, 58] with the
marked transform of [Kol07, Definition 60]): both sides are the marked transform with control m
(weakTransform_eq_markedTransform_of_smooth; the order is preserved by
ordAlongEq_comap_of_smooth, the pulled-back center is smooth over k by
smooth_subschemeι_comap_comp), and the marked transform pulls back in the domain of Definition
60 (markedTransform_comap_blowUpMap_of_pow_dvd, the divisibility F^m ∣ π^* I from
pow_dvd_comap_of_leOrdAlong).
The ⟨j, hj⟩ form for a smooth h with equidimensional source: the induction of
IsOrderSeq.weakTransformSeq_pullback_mk carries the relative dimension n' of h ≫ f
unchanged, since the blow-up of the source along a smooth center is again of relative dimension
n' over k (smoothOfRelativeDimension_blowUpπ_comp_of_smooth), and the morphism of blow-ups
is smooth by base change.
IsOrderSeq.weakTransformSeq_pullback in the ⟨j, hj⟩ form: by induction on the sequence,
peeling one blow-up with isOrderSeq_cons_iff; the blown-up stage is again smooth of relative
dimension n (smoothOfRelativeDimension_blowUpπ_comp_of_smooth) and the morphism of blow-ups
is again smooth of relative dimension d (base change).
IsOrderSeq.weakTransformSeq_pullback for a smooth h with equidimensional source.
Along a smooth pullback of a smooth blow-up sequence of order m for (X, I, E), the induced
ideals of h^* B for h^* I are the pullbacks of the induced ideals of B under the stage lifts:
"I'_i = φ_i^*(I_i)" [Wlo05, Proposition 2.4.2 (2)], for the unmarked transforms of
[Kol07, Definition 66].
Along a smooth blow-up sequence of order ≥ m for (X, I, m, E) the induced marked ideals of
h^* B for (h^* I, m) are the pullbacks of those of B for (I, m) along the stage lifts, for
every h : Y ⟶ X (the iterated form of [Kol07, Lemma 62], without any hypothesis on h), in the
⟨j, hj⟩ form: by induction on the sequence with isOrderGeSeq_cons_iff,
markedTransform_comap_blowUpMap_of_pow_dvd at each stage (the order clause ord_Z I ≥ m gives
F^m ∣ π^* I, pow_dvd_comap_of_leOrdAlong).
The Fin form of IsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom_mk, for every
h : Y ⟶ X (the iterated form of [Kol07, Lemma 62]).
IsOrderGeSeq.markedTransformSeq_pullback in the ⟨j, hj⟩ form: by induction on the sequence
with isOrderGeSeq_cons_iff, markedTransform_comap_blowUpMap_of_pow_dvd at each stage (the order
clause
ord_Z I ≥ m gives F^m ∣ π^* I).
IsOrderGeSeq.markedTransformSeq_pullback for any smooth h, no relative dimension
needed.
Along a smooth pullback of a smooth blow-up sequence of order ≥ m for (X, I, m, E) the
induced marked ideals of h^* B for (h^* I, m) (the transforms of [Kol07, Warning 63 (2)]) are
the pullbacks of those of B for (I, m) [Wlo05, Proposition 2.4.2 (2)].
The induced triple of h^* B, for a smooth h with equidimensional source.
For a smooth blow-up sequence of order m, the induced triple Π_*^{-1}(X, I, E) at the end
of the sequence ([Kol07, Definition 66]) of h^* B for (Y, h^* I, h^{-1} E) is the pullback of
the induced triple of B under the last stage lift [Wlo05, Proposition 2.4.2 (2)].