The principalization sequence is an isomorphism over X ∖ (cosupp I ∪ Sing E)

Clause (3) of [Kol07, Theorem 35] in a corrected form: the principalization Π : X_r → X of (X, I, E) is an isomorphism over X ∖ (cosupp I ∪ Sing E), where Sing E is the locus where two or more components of E meet. Kollár's text says "an isomorphism over X ∖ cosupp I", which overlooks the disjoining blow-ups of [Kol07, 72], whose centers are the loci where several components of E meet; the clause proved here adds Sing E to the excluded set. The proof reads the definition BP T = (disjoinSeq T.E ⧺ BMO_1(X', π^* I, 1, ∑ E^i)) with its empty blow-ups deleted, and shows that every center of both halves avoids the preimage of U := X ∖ (cosupp I ∪ Sing E):

• the disjoining centers lie over Sing E (support_center_disjoinSeq_le; "the subset where k of the components intersect", [Kol07, 72]);
• the BMO_1 centers lie in the cosupport of the marked ideal (π^* I, 1) at their stage (condition (4′) of [Kol07, Definition 66]), and over U the order of π^* I is 0 (ord_eq_zero_iff, support_comap): this is center_disjoint_of_isOrderGeSeq_of_lt at m = 1, from the field isOrderGeSeq of the functor;

so isIso_composite_restrict_of_centers_disjoint applies to both halves, the composite of the concatenation is the composite of the two after the identification of the last stages (composite_concat), restrictions of composites are composites of restrictions (morphismRestrict_comp), and deleting the empty blow-ups does not change the isomorphism locus (isIso_eraseEmpty_composite_restrict).

theorem Hironaka.Sequence.BP_isIso_restrict {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : CategoryTheory.IsIso ((BP T).composite ∣_ (T.I.support ⊔ T.E.singularLocus).compl)

Clause (3) of [Kol07, Theorem 35], with Sing E added to the excluded locus: BP T is an isomorphism over X ∖ (cosupp I ∪ Sing E). The disjoining centers lie over Sing E, the BMO_1 centers lie in the cosupport of π^* I.