The weak transform and the boundary along the componentwise sequence #
The weak transform along the single blow-up π_Z equals the iterated weak transform along the
c blow-ups of the irreducible components, and the final reduced total transforms (Hironaka's
boundaries) agree. Both are read on the end result of the componentwise sequence ofCenters c D,
carried to the single blow-up B_Z X along the canonical isomorphism e of
Hironaka/Resolution/Algebraic/Kol07/ComponentwiseBlowUp.lean.
- Boundary. Hironaka's
E_{i+1} = red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i))[Hir64, Main Theorem II (iii)] depends on supports only: after the whole sequence the boundary is the vanishing ideal ofΠ⁻¹(V(E₀) ∪ V(Z)), and so is the boundary of the single blow-up pulled back alonge, for a reducedE₀(with no blow-up at all the boundary sequence stays atE₀, a radical only whenE₀is reduced). Along an isomorphism the inverse image of a vanishing ideal is the vanishing ideal of the preimage (comap_vanishingIdeal_of_isIso). - Weak transform. The center has snc with the empty family (
hasSncWith_empty_of_smooth), soisOrderSeq_ofCentersapplies withE = ∅. Along a smooth blow-up sequence of orderdHironaka's weak transforms are Kollár's marked transforms ([Kol07, Remark 67];markedTransformSeq_eq_weakTransformSeq), and the marked transform of [Kol07, Definition 60] iterated says the marked transform after the whole sequence is the colon ofΠ^* Jby thed-th power of the product of the centers pulled up to the end result (IsOrderSeq.markedTransformSeq_last_eq_colon: exact division at each stage,colon_pow_eq_of_mul_eq). For the single blow-up the same reads(π_Z^* J) : F_Z^d, andF_Zpulls back alongeto the product of the pulled-up components.
Inverse images along isomorphisms #
The inverse image along an isomorphism is the direct image along its inverse: the two are
adjoint (map_gc) and comap along an isomorphism is invertible.
The inverse image of a vanishing ideal along an isomorphism is the vanishing ideal of the
preimage (Mathlib's map_vanishingIdeal read along the inverse).
The boundary along the componentwise sequence #
The support of a vanishing ideal is the closed set it vanishes on.
The set underlying Hironaka's boundary after the whole componentwise sequence: the preimage
under the composite of V(E₀) ∪ V(Z), Z = ∏ i, D i (no hypotheses; supports only).
Along the componentwise sequence the boundary of a vanishing-ideal boundary stays a vanishing ideal: the vanishing ideal of its own support.
The final reduced total transforms agree, in the general form with the center Z a variable:
Hironaka's boundary after the componentwise sequence of the D i with ∏ i, D i = Z is the
inverse image, under any morphism e over X to B_Z X (necessarily the canonical isomorphism),
of the boundary of the single blow-up, for a reduced E₀.
The final reduced total transforms agree: Hironaka's boundary after the componentwise sequence
of the D i is the inverse image, under any morphism e over X to the blow-up along the product
(necessarily the canonical isomorphism), of the boundary of the single blow-up, for a reduced
E₀.
The components of a regular center (the statements without a field) #
The listed components of a regular closed subscheme have pairwise disjoint supports.
Every center of Z.componentwiseSeq, for a regular Z, is irreducible (towards clause (i) of
[Hir64, Main Theorem II]).
Every center of Z.componentwiseSeq, for a regular Z, is regular (towards clause (i) of
[Hir64, Main Theorem II]).
For a regular center Z, Hironaka's boundary after the componentwise sequence is the inverse
image of the boundary after the single blow-up along Z, for a reduced E₀.
The weak transform along the componentwise sequence #
The marked transform of [Kol07, Definition 60] iterated along a smooth blow-up sequence of
order d (compare [Kol07, Warning 63]): the marked transform after the whole sequence is the colon
of Π^* J by the d-th power of the product of the centers pulled up to the end result. Exact
division at each stage (pow_mul_markedTransform, colon_pow_eq_of_mul_eq) and the colon of a
colon (colon_colon).
The weak transform along π_Z equals the iterated weak transform, in the general form with
the center Z a variable, ∏ i, D i = Z: Hironaka's J_c of the componentwise sequence is the
inverse image, under any morphism e over X to B_Z X, of the weak transform of J along
π_Z. Both are the colon of Π^* J by the d-th power of Π^{-1} Z = ∏ Π^{-1}(D i)
([Kol07, Remark 67]; markedTransformSeq_last_eq_colon).
The weak transform along π_Z equals the iterated weak transform: for a smooth disjoint union
Z = ∏ i, D i of order d along each component, Hironaka's J_c of the componentwise sequence
is the inverse image, under any morphism over X to B_Z X, of the weak transform of J along
π_Z.
The componentwise sequence of a smooth center Z with ord_Z J = d and snc with E is a
smooth blow-up sequence of order d for (X, J, E) [Kol07, Definition 66]: a smooth center is
regular (isRegularLocalRing_stalk), so it is the product of its components.
For a smooth center Z, Hironaka's J_c of the componentwise sequence is the inverse image
of the weak transform along π_Z.