Definition 60 iterated along a sequence: Π^* I = I_r · ∏ Π^*_{r,j+1} F_j^m

Along a blow-up sequence of order ≥ m starting with the marked ideal (I, m), each step satisfies F_{j+1}^m · (I_{j+1}, m) = π_j^* I_j [Kol07, Definition 60, (60.1)], so the pull-back of I to the end result is the last marked transform times the product of the exceptional divisors of the steps, each pulled back along the later steps Π_{r,j+1} and raised to the mark: Π^* I = I_r · ∏_{j<r} Π_{r,j+1}^* F_j^m. This module proves that identity for every sequence and every mark m from the divisibilities F_{j+1}^m ∣ π_j^* I_j alone (a general fact of the markedTransformSeq recursion). The principalization theorem applies it at m = 1 to the marked order reduction functor, where I_r = 𝒪 (Theorem 69 (1), max-ord I_r < 1), which gives Kollár's explicit monomial formula for Π^* I in the proof of Theorem 35 [Kol07, 72].

• exceptionalAt_pow_mul_markedTransformSeq_succ: (60.1) at stage i of a sequence.
• stageMapBetween_zero_comp_eqToHom: Π_{i,0} followed by the cast X_0 = X is Π_i.
• dvd_of_comap_eqToHom_dvd: divisibility of ideal sheaves is reflected by the cast along an equality of schemes.
• comap_composite_eq_markedTransformSeq_last_mul_prod: the iterated formula.

theorem Hironaka.Sequence.exceptionalAt_pow_mul_markedTransformSeq_succ {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (m : ℕ) (i : Fin S.length) (h : S.exceptionalAt i ^ m ∣ (S.markedTransformSeq I m i.castSucc).comap (S.step i)) : S.exceptionalAt i ^ m * S.markedTransformSeq I m i.succ = (S.markedTransformSeq I m i.castSucc).comap (S.step i)

Formula (60.1) of [Kol07, Definition 60] at stage i of a sequence (the recursion (2) of [Kol07, Warning 63]): when F_{i+1}^m divides π_i^* I_i, F_{i+1}^m · (I_{i+1}, m) = π_i^* I_i.

theorem Hironaka.Sequence.stageMapBetween_zero_comp_eqToHom {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (i : Fin (S.length + 1)) : CategoryTheory.CategoryStruct.comp (S.stageMapBetween i 0 ⋯) (CategoryTheory.eqToHom ⋯) = S.stageMap i

Π_{i,0} followed by the cast X_0 = X (stage_zero) is the partial composite Π_i ("Π_i := Π_{i0}", [Kol07, Definition 29]), on either shape of the sequence.

theorem Hironaka.Sequence.dvd_of_comap_eqToHom_dvd {W V : AlgebraicGeometry.Scheme} (e : W = V) {A B : V.IdealSheafData} (h : A.comap (CategoryTheory.eqToHom e) ∣ B.comap (CategoryTheory.eqToHom e)) : A ∣ B

Divisibility of ideal sheaves is reflected by the inverse image along the cast eqToHom e of an equality of schemes.

theorem Hironaka.Sequence.comap_composite_eq_markedTransformSeq_last_mul_prod {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (m : ℕ) : (∀ (i : Fin S.length), S.exceptionalAt i ^ m ∣ (S.markedTransformSeq I m i.castSucc).comap (S.step i)) → I.comap S.composite = S.markedTransformSeq I m (Fin.last S.length) * ∏ j : Fin S.length, (S.exceptionalAt j ^ m).comap (S.stageMapBetween (Fin.last S.length) j.succ ⋯)

Definition 60 iterated along a sequence, the formula behind [Kol07, 72]: when each step satisfies F_{j+1}^m ∣ π_j^* I_j (so that Definition 60 applies, (I_{j+1}, m) = π_j^* I_j / F^m), the pull-back of I to the end result is the last marked transform times the product over the steps of the exceptional divisors, pulled back along the later steps and raised to the mark: Π^* I = I_r · ∏_{j<r} (Π_{r,j+1}^* F_j)^m. By induction on the sequence: the first step is Definition 60 on X, the tail is the induction hypothesis on (π_0)_*^{-1}(I, m), and the j = 0 factor of the product is F_1^m pulled back along Π_{r,1}, the composite of the tail.