The centers of the disjoining sequence are the reduced meet loci

Kollár blows up first Z_0 ⊂ X, "the subset where all the E^i intersect", then Z_1 ⊂ X_1, the subset where k − 1 of the birational transforms intersect, and so on [Kol07, 72]. The center at multiplicity m is defined here as the product ideal sheaf disjoinCenter G m = ∏_{|s| = m} ∑_{i ∈ s} G_i (the scheme structure ∑_{i∈s} G_i on each m-fold intersection), and Disjoin/Reduced.lean shows that at each step this is the reduced subscheme on the meet locus once no (m+1)-fold intersections remain (disjoinCenter_eq_vanishingIdeal). This module iterates that fact along the sequence: the invariant "no (m+1)-fold intersections" is carried by meetLocus_strictTransform_disjoinCenter (Disjoin/Step.lean), the running family stays inside an snc family by isSnc_totalTransform_disjoinCenter, so that every center Z_t of disjoinSeq E is Kollár's subset with its reduced structure.

• center_disjoinSeqAux_eq_vanishingIdeal: the invariant along disjoinSeqAux;
• center_disjoinSeq_eq_vanishingIdeal: for disjoinSeq E, the center at step t is the reduced subscheme on the locus where card E.ι − t of the current birational transforms meet.

theorem Hironaka.Sequence.center_disjoinSeqAux_eq_vanishingIdeal {k : Type u} [Field k] [PerfectField k] {ι : Type u_1} [Fintype ι] (m : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} : F.IsSnc → ∀ (G : ι → X.IdealSheafData), (∀ (i : ι), G i ∈ Set.range F.component) → meetLocus G (m + 1) = ⊥ → ∀ (i : Fin (disjoinSeqAux m G).length), (disjoinSeqAux m G).center i = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (meetLocus (fun (a : ι) => (disjoinSeqAux m G).strictTransformSeq (G a) i.castSucc) (m - ↑i))

The invariant along the disjoining steps [Kol07, 72]: with no (m+1)-fold intersections among the current transforms, the center at step i is the reduced subscheme on the locus where m − i of the current birational transforms meet.

theorem Hironaka.Sequence.center_disjoinSeq_eq_vanishingIdeal {k : Type u} [Field k] [PerfectField k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) (i : Fin (disjoinSeq E).length) : (disjoinSeq E).center i = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (meetLocus (fun (a : E.ι) => (disjoinSeq E).strictTransformSeq (E.component a) i.castSucc) (Fintype.card E.ι - ↑i))

The center of the t-th disjoining blow-up is the reduced subscheme on Kollár's subset [Kol07, 72]: the locus where card E.ι − t of the current birational transforms of the components meet.