Restriction to a closed subscheme: the stage embeddings and Kollár's warning

The restriction j^* B = B|_S of a blow-up sequence to a closed subscheme S = V(J) [Kol07, 30.2] is the pullback along J.subschemeι; its stage lifts S_i → X_i are closed immersions onto the strict transforms of S (Hironaka/Scheme/BlowUpSequence/Restrict.lean). This module restates that fact for the closed immersion J.subschemeι (isClosedImmersion_pullbackStageHom_subschemeι) and records, as an example, the precise sense in which "the restriction of a smooth blow-up sequence need not be a smooth blow-up sequence" [Kol07, 30.2]. On the model of HironakaExamples/Sequence/CuspModel.lean (X = 𝔸²_k, the center V(x, y), the cuspidal cubic S = V(y² − x³)), blowing up the origin is a smooth blow-up sequence whose restriction to the cusp starts at a scheme that is not smooth over k (HironakaExamples/Sequence/CuspWitness.lean). The predicate IsSmooth of this library asks only that the centers be smooth, and the restricted sequence does satisfy it: its one center V(x, y) ∩ V(y² − x³) = Spec k is smooth. What fails is the ambient clause of [Kol07, Notation 19], the smoothness of the stages themselves.

theorem Hironaka.Sequence.isClosedImmersion_pullbackStageHom_subschemeι {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (i : Fin (S.length + 1)) : AlgebraicGeometry.IsClosedImmersion (S.pullbackStageHom J.subschemeι i)

The natural embeddings S_i ↪ X_i of the restriction to V(J) are closed immersions [Kol07, 30.2]; the case of J.subschemeι of isClosedImmersion_pullbackStageHom.