Clause (2) of Theorem 35: the pull-back of the ideal is monomial

From the proof of the principalization theorem [Kol07, 72]: by construction Π^*_{(X,I,E)} I is I_r · 𝒪_{X_r}(F) for an effective divisor F supported on the total transform of ∑ E^i; here I_r = 𝒪_{X_r} since max-ord I_r < 1, and F is a simple normal crossing divisor, so Π^*_{(X,I,E)} I is a monomial ideal "which can be written down explicitly": with F_j ⊂ X_{j+1} the exceptional divisor of the jth step, Π^*_{(X,I,E)} I = 𝒪_{X_r}(−∑_{j=s}^{r−1} Π^*_{r,j+1} F_j). Two theorems:

• BMO_one_comap_composite_eq_prod, the explicit formula on the BMO_1 part (Kollár's sum over j = s, …, r − 1): the marked transform of [Kol07, Definition 60] iterated along the sequence (comap_composite_eq_markedTransformSeq_last_mul_prod) with the exact division at each mark-1 step (F_{j+1} ∣ π_j^* I_j, from the order condition of [Kol07, Definition 66] through pow_dvd_comap_of_leOrdAlong) and I_r = 𝒪 from [Kol07, Theorem 69 (1)] (max-ord I_r < 1, dimFreeBMO_maxOrd_lt);
• BP_isIdealOfSncDivisor, clause (2) of [Kol07, Theorem 35] as IsIdealOfSncDivisor (Π^* I): the disjoining part enters only through π^* I (the ideal of the disjoined triple), the BMO_1 part is the explicit product, which is the ideal sheaf of an effective divisor supported on a simple normal crossing family (isIdealOfSncDivisor_prod_comap_exceptionalAt), and the property is carried across the two isomorphisms of the definition, the cast of concat and the deletion of the empty blow-ups, by IsIdealOfSncDivisor.comap_of_smooth.

theorem Hironaka.Sequence.BMO_one_comap_composite_eq_prod {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.BMOClassFree 1 T) : T.I.comap ((Stage.BMO_m 1 k).seq T hT).composite = ∏ j : Fin ((Stage.BMO_m 1 k).seq T hT).length, (((Stage.BMO_m 1 k).seq T hT).exceptionalAt j).comap (((Stage.BMO_m 1 k).seq T hT).stageMapBetween (Fin.last ((Stage.BMO_m 1 k).seq T hT).length) j.succ ⋯)

"Π^*_{(X,I,E)} I = 𝒪_{X_r}(−∑_{j=s}^{r−1} Π^*_{r,j+1} F_j)" [Kol07, 72]: along the BMO_1 part, the order reduction functor for marked ideals at mark 1 on any marked triple of mark 1, the pull-back of the ideal to the end result is the product of the exceptional divisors of the steps pulled back along the later steps; I_r = 𝒪 since max-ord I_r < 1.

theorem Hironaka.Sequence.BP_isIdealOfSncDivisor {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : (T.I.comap (BP T).composite).IsIdealOfSncDivisor

Clause (2) of [Kol07, Theorem 35]: the pull-back of I along BP T is the ideal sheaf of an effective divisor supported on a simple normal crossing family. The disjoining part contributes only π^* I, the ideal of the disjoined triple on which the BMO_1 part runs [Kol07, 72], and the pull-back along the BMO_1 part is the explicit product ∏_j Π_{r,j+1}^* F_j of BMO_one_comap_composite_eq_prod, the ideal sheaf of an snc divisor by isIdealOfSncDivisor_prod_comap_exceptionalAt; the two isomorphisms in the definition (the cast of the concatenation and the deletion of the empty blow-ups) transport the property (IsIdealOfSncDivisor.comap_of_smooth).