At the first containing stage the centre is the strict transform near it

Włodarczyk runs the algorithm until "the strict transform of one of the components Yᵢ is the center" ([Wlo05, Theorem 4.7.1, proof]). For the loop BED (Hironaka.Resolution.Algebraic.Wlo05.Embedded) this is made precise as follows: at the FIRST stage j of a smooth blow-up sequence of order ≥ m ≥ 1 whose centre Z_j contains the strict transform c̃_j of a component c = V(closure {η}) of V(I) (with η off the boundary and I = c at η), the centre coincides with c̃_j at every point of c̃_j: (Z_j)_p = (c̃_j)_p for all p ∈ c̃_j. So the absorbing centre is c̃_j on a neighbourhood of c̃_j, and no other component of Z_j meets it.

The proof is the argument of the proof of [Kol07, Corollary 22] in the general form isOpenImmersion_inclusion_of_isGenericPoint of Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification: the lifted generic point η' of c̃_j (GenericLift, exists_genericLift, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedGenericLift) is a generic point of V(I_j); the centre lies in V(I_j) (the order condition, IsOrderGeSeq.leOrdAlong), so η' is a maximal point of Z_j; c̃_j is integral and Z_j is regular (smooth over k, isRegular_of_smooth), hence V(c̃_j) ⟶ V(Z_j) is an open immersion and the stalk ideals agree along c̃_j (stalkIdeal_eq_of_isOpenImmersion_inclusion, Hironaka.Resolution.Algebraic.Snc.RestrictSubscheme). Nothing here uses the hypothesis ClaimKC of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses, which is false for the transcribed order; stalkIdeal_center_eq_of_absorbed of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedAbsorbed is the conditional form of the same statement. This observation is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry.

theorem Hironaka.Resolution.stalkIdeal_center_eq_strictTransformSeq_of_first {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} (hS : S.IsOrderGeSeq f I m E) (hm : 1 ≤ m) {η : ↥X} (hη : η ∈ I.support.genericPoints) (hηE : ∀ (i : E.ι), η ∉ (E.component i).support) (hIc : I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (j : Fin S.length) (hle : S.center j ≤ S.strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) j.castSucc) (hmin : ∀ l < ↑j, ¬CenterContains S (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) l) (p : ↥(S.stage j.castSucc)) : p ∈ (S.strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) j.castSucc).support → (S.center j).stalkIdeal p = (S.strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) j.castSucc).stalkIdeal p

Along a smooth blow-up sequence of order ≥ m ≥ 1 for (I, m, E) on a Noetherian X, at a stage j whose centre contains the strict transform of c = vanishingIdeal (closure {η}) (η a generic point of V(I) off the boundary at which I = c) while no earlier centre does, the centre and the strict transform have the same stalk ideal at every point of the strict transform (the argument of the proof of [Kol07, Corollary 22]).

theorem Hironaka.Resolution.stalkIdeal_center_eq_strictTransformSeq_bmoOneRun {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (j : Fin (bmoOneRun T hm).length) (hle : (bmoOneRun T hm).center j ≤ (bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) j.castSucc) (hmin : ∀ l < ↑j, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) l) (p : ↥((bmoOneRun T hm).stage j.castSucc)) : p ∈ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) j.castSucc).support → ((bmoOneRun T hm).center j).stalkIdeal p = ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) j.castSucc).stalkIdeal p

The identity of the centre and the strict transform for one run of BMO_1 (bmoOneRun, the round of the loop): the first centre containing the strict transform of a member c = vanishingIdeal (closure {η}) agrees with it stalkwise along it.

theorem Hironaka.Resolution.stalkIdeal_center_eq_strictTransformSeq_find {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (hcC : AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η}) ∈ C) (hcc : CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) (Nat.find h)) (p : ↥((bmoOneRun T hm).stage ⟨Nat.find h, ⋯⟩)) : p ∈ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ⟨Nat.find h, ⋯⟩).support → ((bmoOneRun T hm).center ⟨Nat.find h, ⋯⟩).stalkIdeal p = ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ⟨Nat.find h, ⋯⟩).stalkIdeal p

The identity at the truncation index of the loop (the Nat.find of bedAux, the first stage with an absorption): a member c = vanishingIdeal (closure {η}) of C absorbed there is the centre near its strict transform, since no earlier stage absorbs any member, so none contains c̃.