The disjoining centers lie over Sing E

Clause (3) of the principalization theorem as proved in this library (exists_functorial_principalization) says that Π is an isomorphism over X ∖ (cosupp I ∪ Sing E), where Sing E is the locus where two components of E meet, rather than over X ∖ cosupp I as printed in [Kol07, Theorem 35 (3)]: the disjoining sequence of [Kol07, 72] blows up the intersections of the components of E regardless of I. The fact behind this form of the clause is that every center of the disjoining sequence lies over Sing E: a center is a locus where at least two birational transforms of components meet, and a birational transform lies over its component.

• support_center_disjoinSeqAux_le: the invariant form: members lying over distinct components of a family E₀ through a morphism π have all their disjoining centers over Sing E₀.
• support_center_disjoinSeq_le: the statement for the disjoining sequence.

theorem Hironaka.Sequence.mem_sing_of_mem_meetLocus_two {X X₀ : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] {G : ι → X.IdealSheafData} (π : X ⟶ X₀) (E₀ : X₀.DivisorFamily) (e : ι → E₀.ι) (he : Function.Injective e) (hover : ∀ (i : ι), ∀ x ∈ (G i).support, π x ∈ (E₀.component (e i)).support) {x : ↥X} {m : ℕ} (hm : 2 ≤ m) (hx : x ∈ meetLocus G m) : π x ∈ E₀.singularLocus

Two members through a point, lying over distinct components, put the image in Sing E₀.

theorem Hironaka.Sequence.support_center_disjoinSeqAux_le (m : ℕ) {X X₀ : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (π : X ⟶ X₀) (E₀ : X₀.DivisorFamily) (e : ι → E₀.ι) : Function.Injective e → (∀ (i : ι), ∀ x ∈ (G i).support, π x ∈ (E₀.component (e i)).support) → ∀ (i : Fin (disjoinSeqAux m G).length), ∀ x ∈ ((disjoinSeqAux m G).center i).support, (CategoryTheory.CategoryStruct.comp ((disjoinSeqAux m G).stageMap i.castSucc) π) x ∈ E₀.singularLocus

Every center of the disjoining steps lies over Sing E₀ when the members lie over distinct components of E₀.

theorem Hironaka.Sequence.support_center_disjoinSeq_le {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (i : Fin (disjoinSeq E).length) : ((disjoinSeq E).center i).support ≤ E.singularLocus.preimage ⋯

Every center of the disjoining sequence lies over Sing E: it is a locus where at least two birational transforms of components of E meet. This is why clause (3) of the principalization theorem excludes Sing E together with cosupp I.