The conclusion of Włodarczyk's Claim descends along the local cover of Theorem 105

[Kol07, Theorem 105] evaluates BO_{n,1} on a triple T through a local cover g : T'.X.left → T.X.left (a coproduct of open immersions, surjective) on whose pieces a smooth hypersurface of maximal contact exists: BO(T') = g^* BO(T), since the functor commutes with smooth morphisms ([Kol07, Theorem 103 (2)], commutesWithSmooth). The conclusion of Włodarczyk's Claim in the proof of [Wlo05, Theorem 4.7.1] (ClaimFor, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimAt) for the run on T at a point p of the strict transform c̃_i follows from the conclusion for the pulled-back run on T' at a point q over p, for the member c' := I_{closure η'} of a suitable point η' over η (a component of g⁻¹(V(c)) through the image of q, coe_support_strictTransformSeq_biUnion): the first containing stage is the same on both sides (the lifted generic points correspond, GenericLift.uniq), and the stalk identity descends along the stalk isomorphism of the stage lift (openImmersionCoprods_pullbackStageHom). The commutation with smooth morphisms is [Kol07, 34.1]. The same bookkeeping, with the chain-relative conclusion, is cp1For_of_pullback_cover (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Cover).

The stop rule through the lifted generic point

theorem Hironaka.Resolution.centerContains_iff_mem_center_support {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (c : X.IdealSheafData) {l : ℕ} (hl : l < S.length) {ζ : ↥(S.stage ⟨l, ⋯⟩)} (hζ : S.strictTransformSeq c ⟨l, ⋯⟩ = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {ζ})) : CenterContains S c l ↔ ζ ∈ (S.center ⟨l, hl⟩).support

When the strict transform at stage l is the reduced ideal of the closure of ζ, the centre at l contains it iff ζ lies on the centre.

theorem Hironaka.Resolution.center_pullback_mk' {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (g : Y ⟶ X) {l : ℕ} (hl : l < S.length) (hl' : l < (S.pullback g).length) : (S.pullback g).center ⟨l, hl'⟩ = (S.center ⟨l, hl⟩).comap (S.pullbackStageHom g ⟨l, ⋯⟩)

The centre of the pulled-back sequence at l, in the mk form of the indices.

theorem Hironaka.Resolution.stageMap_pullbackStageHom_apply {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (g : Y ⟶ X) (i : Fin (S.length + 1)) (y : ↥((S.pullback g).stage (S.pullbackStageIdx g i))) : (S.stageMap i) ((S.pullbackStageHom g i) y) = g (((S.pullback g).stageMap (S.pullbackStageIdx g i)) y)

The stage lift applied to a point, followed by the stage map: the image of the pulled-back stage map.

theorem Hironaka.Resolution.claimFor_of_pullback_cover {k : Type u} [Field k] [CharZero k] (T T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ T.X.left) (hg : AlgebraicGeometry.openImmersionCoprods g) (hsurj : Function.Surjective ⇑g) (hpb : T'.IsPullbackOf T g) (S : T.X.left.BlowUpSequence) (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 T.E) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (j : T.E.ι), η ∉ (T.E.component j).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (h : ∀ (η' : ↥T'.X.left), g η' = η → η' ∈ T'.I.support.genericPoints → (∀ (j : T'.E.ι), η' ∉ (T'.E.component j).support) → T'.I.stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η' → ClaimFor (S.pullback g) T'.I T'.E 1 η') : ClaimFor S T.I T.E 1 η

The conclusion of Włodarczyk's Claim descends along a coproduct of open immersions ([Kol07, Theorem 105]): if it holds for the pulled-back run on T' at every point η' over η that is a generic point of g⁻¹(V(c)) (with the member I_{closure η'}), it holds for the run on T at η.