The disjoining center is the reduced subscheme on Kollár's subset

Kollár blows up "the subset Z_t where k − t of the transforms intersect" [Kol07, 72], a closed subset, so the blow-up center is its reduced closed subscheme. The center used here, disjoinCenter G (m+1) = ∏_{|s| = m+1} ∑_{i ∈ s} G_i, has that subset as its support (support_disjoinCenter); this module shows that under the standing hypotheses (members of an snc family with no (m+2)-fold intersections) it is the reduced subscheme: its stalk at a point of the meet locus is generated by part of a regular system of parameters, a prime ideal (isRegularLocalRing_quotient_span_image_finset), and off the meet locus it is the unit ideal, so it is a radical ideal sheaf, and the vanishing ideal sheaf of its support is its radical (Mathlib's vanishingIdeal_support).

• stalkIdeal_radical: the stalk of the radical is the radical of the stalk (the stalk is a localization of the sections over any affine neighbourhood, and localization commutes with radicals).
• disjoinCenter_eq_vanishingIdeal: the center is the reduced subscheme on Kollár's subset.

theorem Hironaka.Sequence.stalkIdeal_radical {X : AlgebraicGeometry.Scheme} (J : X.IdealSheafData) (x : ↥X) : J.radical.stalkIdeal x = (J.stalkIdeal x).radical

The stalk of the radical of an ideal sheaf is the radical of its stalk: the stalk is the localization of Γ(X, U) at the prime of x for any affine U ∋ x (IsAffineOpen.isLocalization_stalk), and localization commutes with radicals.

theorem Hironaka.Sequence.radical_eq_self_of_forall_stalkIdeal {X : AlgebraicGeometry.Scheme} (J : X.IdealSheafData) (h : ∀ (x : ↥X), (J.stalkIdeal x).radical = J.stalkIdeal x) : J.radical = J

An ideal sheaf whose stalks are all radical is radical.

theorem Hironaka.Sequence.disjoinCenter_eq_vanishingIdeal {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} (hF : F.IsSnc) {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (hG : ∀ (i : ι), G i ∈ Set.range F.component) (m : ℕ) (hm : meetLocus G (m + 2) = ⊥) : disjoinCenter G (m + 1) = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (meetLocus G (m + 1))

For members of an snc family with no (m+2)-fold intersections, the center at multiplicity m + 1 is the reduced subscheme on the meet locus: blowing it up is blowing up Kollár's subset [Kol07, 72].