Restriction of a blow-up sequence to a closed subscheme #
For a closed subscheme j : S ↪ X and a blow-up sequence B starting with X, the restriction
j^* B = B|_S of [Kol07, 30.2] is the sequence starting with S whose centers are Z_i ∩ S_i,
with S_{i+1} = B_{Z_i ∩ S_i} S_i "naturally identified with the birational transform
(π_i)⁻¹_* S_i ⊂ X_{i+1}" (Kollár cites [Har77, Proposition II.7.15]), "thus there are natural
embeddings
S_i ↪ X_i".
Here the restriction is the pullback S.pullback J.subschemeι of
Hironaka/Scheme/BlowUpSequence/Pullback.lean (the inverse image ideal D.comap J.subschemeι is
the ideal of Z ∩ S in S), and the natural embedding of one step is the morphism of blow-ups
blowUpMap J.subschemeι D.
The one-step statement, that this morphism is a closed immersion with kernel the strict transform,
is proved in Hironaka/Scheme/BlowUp/ClosedImmersionLift.lean: B_{Z ∩ S} S is isomorphic to the
strict transform V(Jˢ) ⊆ B_Z X compatibly with the maps to X ([Har77, Proposition II.7.15],
exists_iso_strictTransform_subscheme); the composite e.hom ≫ (strictTransform D J).subschemeι
is therefore a morphism over J.subschemeι, hence equal to the lift by the uniqueness clause of
the universal property (eq_blowUpMap), and an isomorphism followed by a closed immersion is a
closed immersion.
This module proves the stagewise statements. From the one-step case (for every closed immersion
j, blowUpMap j D is a closed immersion with kernel strictTransform D j.ker,
AlgebraicGeometry.isClosedImmersion_blowUpMap_of_isClosedImmersion and
AlgebraicGeometry.ker_blowUpMap_of_isClosedImmersion, through the scheme-theoretic image of j),
by induction every stage lift S.pullbackStageHom j i is a closed immersion with kernel
S.strictTransformSeq j.ker i (isClosedImmersion_pullbackStageHom, ker_pullbackStageHom);
Kollár's "S_{i+1} is naturally identified with the birational transform (π_i)⁻¹_* S_i" is the
isomorphism exists_iso_strictTransformSeq onto the subscheme of that kernel, given by Mathlib's
Scheme.Hom.toImage. When every center Z_i lies in the strict transform S_i, the restricted
sequence of a smooth sequence is smooth (isSmooth_pullback_of_strictTransformSeq_le): the
smoothness of Z_i ⊆ S_i is transported along the isomorphism V(Z_i ∩ S_i) ≅ V(Z_i) of
isPullback_of_isClosedImmersion (exists_iso_subscheme_comap_of_ker_le), whose ideal-sheaf form
(Z.comap g).map g = Z for g.ker ≤ Z (map_comap_of_ker_le) is used in
Hironaka/Scheme/BlowUpSequence/Pushforward.lean for j_* j^* B = B.
Stagewise: the natural embeddings S_i ↪ X_i #
Every stage lift of the pullback along a closed immersion is a closed immersion, in the
⟨n, hn⟩ form of the indices.
The kernel of the n-th stage lift is the n-th strict transform of the image of j, in the
⟨n, hn⟩ form of the indices.
Every stage lift of the pullback along a closed immersion is a closed immersion: the natural
embeddings S_i ↪ X_i of [Kol07, 30.2].
The kernel of the i-th stage lift is the i-th strict transform of the image of j: the
image of S_i ↪ X_i is (Π_i)⁻¹_* S.
The i-th stage of the restriction to V(J) is isomorphic to the strict transform
S.strictTransformSeq J i, the isomorphism followed by the strict transform's inclusion being the
natural embedding pullbackStageHom ([Kol07, 30.2], citing [Har77, Proposition II.7.15]).
Centers inside the strict transforms #
For a closed immersion g : Y ⟶ X whose kernel lies in Z (V(Z) ⊆ Y), the closed subscheme
of the inverse image ideal Z.comap g is V(Z) itself, compatibly with the inclusions into X:
the fibre product V(Z) ×_X Y is V(Z) (Mathlib's isPullback_of_isClosedImmersion).
If every center Z_i is a closed subscheme of the strict transform S_i of V(J) and S is
a smooth blow-up sequence, its restriction to V(J) is a smooth blow-up sequence on V(J): the
restricted center Z_i ∩ S_i is Z_i itself (exists_iso_subscheme_comap_of_ker_le for the
stage lift, whose kernel is S_i). This is the situation of a hypersurface of maximal contact
[Kol07, Definition 78].
For a closed immersion g and a closed subscheme Z of its image (g.ker ≤ Z), pushing the
restriction Z ∩ g(Y) forward gives Z back: (Z.comap g).map g = Z. The IsIso case is
map_comap_of_isIso (Hironaka/Scheme/BlowUp/Glue/Trivial.lean); this is the closed-immersion
form, through the isomorphism exists_iso_subscheme_comap_of_ker_le.