The centers of the principalization sequence are smooth and have normal crossings with E

Clause (1) of [Kol07, Theorem 35]: every center of BP(X, I, E) is smooth and has simple normal crossings with the running total transform of E [Kol07, Definition 25]. The two halves of the definition give this for their own boundaries: disjoinSeq_isSmooth and disjoinSeq_hasSncWith for the disjoining part against E itself, and the field isOrderGeSeq of the functor BMO_1 (the order condition of [Kol07, Definition 66]) for the BMO_1 part against Kollár's ordered family ∑ E^i. But ∑ E^i is the total transform of E at the end of the disjoining sequence with the birational transforms of the original components collapsed into the one member E^0 ("in (68) we allow the components of E to be reducible", [Kol07, 72]). Reading the clause against the original E is a regrouping: the uncollapsed total transform subdivides the collapsed one (subdivides_collapse; at any point at most one of the pairwise disjoint final strict transforms passes, meetLocus_strictTransformSeq_disjoinSeq, so the collapsed member has the stalk of that one member), and simple normal crossings pass to subdivisions along the whole sequence (isOrderGeSeq_of_subdivides, the marked analogue of isOrderSeq_of_subdivides, both in Hironaka/Resolution/Algebraic/Kol07/RefineFamily.lean).

The bookkeeping vehicle is IsOrderGeSeq at mark 0: its order clause is vacuous (LeOrdAlong _ 0), so S.IsOrderGeSeq f ⊤ 0 E says exactly "the centers of S are smooth and have simple normal crossings with the total transforms of E", and the concatenation and empty-blow-up transports for it are available (isOrderGeSeq_concat, IsOrderGeSeq.eraseEmpty). BP_isOrderGeSeq_zero assembles them; BP_center_smooth_hasSncWith reads off clause (1).

theorem Hironaka.Sequence.disjoinedFamily_collapse_disjoint {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) (x : ↥(disjoinSeq E).last) (a b : ((disjoinSeq E).totalTransformSeq E (Fin.last (disjoinSeq E).length)).ι) : a ∈ Set.range ((disjoinSeq E).originalIdx E (Fin.last (disjoinSeq E).length)) → b ∈ Set.range ((disjoinSeq E).originalIdx E (Fin.last (disjoinSeq E).length)) → x ∈ (((disjoinSeq E).totalTransformSeq E (Fin.last (disjoinSeq E).length)).component a).support → x ∈ (((disjoinSeq E).totalTransformSeq E (Fin.last (disjoinSeq E).length)).component b).support → a = b

"After (k − 1) steps we get rid of all pairwise intersections" [Kol07, 72], as the disjointness hypothesis of subdivides_collapse for the collapse defining collapsedFamily: the final birational transforms of two members of E never meet (meetLocus_strictTransformSeq_disjoinSeq; the argument of disjoinedFamily_isSnc).

theorem Hironaka.Sequence.BP_isOrderGeSeq_zero {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : (BP T).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) ⊤ 0 T.E

Clause (1) of [Kol07, Theorem 35] in the vehicle IsOrderGeSeq at mark 0, whose order clause is vacuous: BP T is a smooth blow-up sequence whose centers have simple normal crossings with the total transforms of the original E. The disjoining part has this by construction, the BMO_1 part by the order condition of [Kol07, Definition 66] for the collapsed ∑ E^i, regrouped to the total transform of E through subdivides_collapse and isOrderGeSeq_of_subdivides; the two are concatenated by isOrderGeSeq_concat and the empty blow-ups deleted by IsOrderGeSeq.eraseEmpty.

theorem Hironaka.Sequence.BP_center_smooth_hasSncWith {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (i : Fin (BP T).length) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp ((BP T).center i).subschemeι (CategoryTheory.CategoryStruct.comp ((BP T).stageMap i.castSucc) (T.X.left ↘ AlgebraicGeometry.Spec ↧k))) ∧ ((BP T).totalTransformSeq T.E i.castSucc).HasSncWith ((BP T).center i)

Clause (1) of [Kol07, Theorem 35]: every center of BP T is smooth over k and has simple normal crossings with the total transform of E at its stage; read off BP_isOrderGeSeq_zero.