The ideal-theoretic strict transforms of a closed subspace along a blow-up sequence #
A closed subspace Y ⊆ M, given by its ideal sheaf J, is carried along a finite blow-up sequence
π_0, …, π_{r-1} with smooth centres by its strict transforms Y_0 = Y, Y_{k+1} = (π_k)^{-1}_* Y_k: the stages of Kollár's restricted sequence [Kol07, Definition 30.2] and the
strict transforms Ỹ_Z ⊂ Ũ_Z in Włodarczyk's canonical embedded desingularization of a germ Wlo09,
§4, (2)⇒(3) and (3)⇒(4). On manifolds each step is the strict transform of a closed subspace under
one blowing-up (strictTransformSubspace: the saturation of the total transform by the exceptional
divisor, [BM97, §3, Proposition 3.13]), taken at the witnesses of the k-th blow-up
(FiniteSuccession.isClosedSubmanifold_center, FiniteSuccession.isBlowUp_map). This is the
ideal-level counterpart of the set-level FiniteSuccession.strictTransformSeq, and
exactly the recursion that the fields transform_zero/transform_succ of
AmbientBlowUpFactorization spell out for the chain Y_0, …, Y_r: for the chain defined here both
fields hold by rfl.
The chain itself, FiniteSuccession.strictTransformSubspaceSeq S J i (the strict transform
Y_i ⊆ U_i of the closed subspace J of M at stage i, by recursion on i), is statement
vocabulary and lives in Hironaka/Manifold/FiniteSuccession/Defs.lean; this file holds its two
defining equations.
The chain starts with Y_0 = J (the field transform_zero of
AmbientBlowUpFactorization).
Y_{i+1} is the strict transform of Y_i under the i-th blow-up at the succession's
witnesses (the field transform_succ of AmbientBlowUpFactorization).