The smooth window at a regular point of Y, and clause (b) for BED

At a point q of Y = V(I) smooth over k the embedded desingularization sequence BED(X, I_Y, ∅) (Hironaka.Resolution.Algebraic.Wlo05.Embedded) has no centre with a point over ι q: clause (b) of [Wlo05, Theorem 1.0.2] ("all centers Cᵢ are disjoint from the set Reg(Y)"), in the stronger form in which the point need not lie on the strict transform of Y (BED_center_disjoint_reg).

• isPrime_stalkIdeal_of_mem_smoothLocus, eq_of_specializes_of_mem_smoothLocus: at a smooth point of V(I) the stalk I_x is prime (𝒪_{V(I),q} is a regular local ring, mem_smoothLocus_iff_isRegularAt, hence a domain), so exactly ONE irreducible component of V(I) passes through it (the minimal primes of I_x are the components' stalks).
• isReduced_subscheme_vanishingIdeal, isReduced_subscheme_comap_of_isOpenImmersion: the reduced components are reduced (radical stalks), and reducedness descends to an open subscheme.
• exists_smoothWindow_of_mem_smoothLocus: the window — an affine open W ∋ ι q inside the complement of ι(Y ∖ Reg Y) (closed: ι is a closed immersion) and of the other components (a finite union of closed sets) is a smooth window (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedSmoothWindow) for (X, I_Y, 1, ∅) and the loop's member set: the boundary is empty, I|_W = I_c|_W (both radical with the same support), the component c is integral, V(c) ∩ W = V(I) ∩ W ⊆ Reg(Y) is smooth over k (preimage_smoothLocus_eq on the open piece of V(I)), and no other member meets W.
• BED_center_disjoint_reg: clause (b), by centersMiss_BED_of_smoothWindow on that window; the form used by Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses.

Reduced components

theorem Hironaka.Resolution.isReduced_subscheme_vanishingIdeal {X : AlgebraicGeometry.Scheme} (Z : TopologicalSpace.Closeds ↥X) : AlgebraicGeometry.IsReduced (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z).subscheme

The closed subscheme of a vanishing ideal is reduced: its stalks are the quotients of the stalks of X by the stalks of vanishingIdeal Z, which are radical (vanishingIdeal Z is its own radical, vanishingIdeal_support; stalkIdeal_radical).

theorem Hironaka.Resolution.isReduced_subscheme_comap_of_isOpenImmersion {X W : AlgebraicGeometry.Scheme} (h : W ⟶ X) [AlgebraicGeometry.IsOpenImmersion h] (I : X.IdealSheafData) [AlgebraicGeometry.IsReduced I.subscheme] : AlgebraicGeometry.IsReduced (I.comap h).subscheme

Reducedness of V(I) descends to V(h^* I) along an open immersion h: V(h^* I) is isomorphic to the fibre product W ×_X V(I) (Mathlib's comapIso), an open subscheme of V(I).

The unique component through a smooth point of Y

theorem Hironaka.Resolution.isPrime_stalkIdeal_of_mem_smoothLocus {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) {q : ↥TX.I.subscheme} (hq : q ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp TX.I.subschemeι (TX.X.left ↘ AlgebraicGeometry.Spec ↧k))) : (TX.I.stalkIdeal (TX.I.subschemeι q)).IsPrime

At a point q of V(I) smooth over k the stalk I_{ι q} is prime: 𝒪_{V(I),q} is a regular local ring (mem_smoothLocus_iff_isRegularAt), hence a domain, and it is the quotient of 𝒪_{X, ι q} by I_{ι q} (stalkQuotientEquiv).

theorem Hironaka.Resolution.eq_of_specializes_of_mem_smoothLocus {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) {q : ↥TX.I.subscheme} (hq : q ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp TX.I.subschemeι (TX.X.left ↘ AlgebraicGeometry.Spec ↧k))) {η η' : ↥TX.X.left} (hη : η ∈ TX.I.support.genericPoints) (hη' : η' ∈ TX.I.support.genericPoints) (h1 : η ⤳ TX.I.subschemeι q) (h2 : η' ⤳ TX.I.subschemeι q) : η = η'

Two generic points of V(I) specializing to a point where V(I) is smooth over k coincide: the stalks of their reduced components are minimal primes of the PRIME I_x (stalkIdeal_vanishingIdeal_mem_minimalPrimes), hence both equal to I_x (eq_of_stalkIdeal_vanishingIdeal_closure_eq).

theorem Hironaka.Resolution.exists_smoothWindow_of_mem_smoothLocus {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (hE : IsEmpty TX.E.ι) [AlgebraicGeometry.IsReduced TX.I.subscheme] {q : ↥TX.I.subscheme} (hq : q ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp TX.I.subschemeι (TX.X.left ↘ AlgebraicGeometry.Spec ↧k))) : ∃ (W : TX.X.left.Opens), AlgebraicGeometry.IsAffineOpen W ∧ TX.I.subschemeι q ∈ W ∧ SmoothWindow { toTriple := TX, m := 1 } (componentIdeals TX) W.ι

The smooth window at a regular point of Y ([Wlo05, 4.6]) — for q ∈ Reg(Y) there is an affine open W ∋ ι q of X which is a smooth window for (X, I_Y, 1, ∅) and the loop's member set: W misses ι(Y ∖ Reg Y) (closed, ι a closed immersion) and every irreducible component of Y other than the one through ι q (finitely many, closed); on it the boundary is empty, I_Y|_W = I_c|_W (radical ideals with the same support), the component c is integral, V(c) ∩ W ⊆ Reg(Y) is smooth over k, and no other member meets W.

Clause (b)

theorem Hironaka.Resolution.BED_center_disjoint_reg {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (hE : IsEmpty TX.E.ι) [AlgebraicGeometry.IsReduced TX.I.subscheme] (i : Fin (BED TX).length) (x : ↥((BED TX).stage i.castSucc)) : x ∈ ((BED TX).center i).support → x ∈ ((BED TX).strictTransformSeq TX.I i.castSucc).support → ((BED TX).stageMap i.castSucc) x ∉ ⇑TX.I.subschemeι '' ↑(AlgebraicGeometry.Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp TX.I.subschemeι (TX.X.left ↘ AlgebraicGeometry.Spec ↧k)))

Clause (b) of [Wlo05, Theorem 1.0.2] — no point of a centre of BED TX maps to a point of Reg(Y). The hypothesis that x lies on the strict transform of Y is present because clause (b) speaks of the points of the strict transform Y_i over Reg(Y); the proof does not need it, because the stronger statement holds — no point of a centre at all maps to a smooth point of Y, Włodarczyk's literal (b) — by the smooth window at the regular point and centersMiss_BED_of_smoothWindow.