A centre of order at least two never contains a reduced component

Włodarczyk's Claim in the proof of [Wlo05, Theorem 4.7.1] is about the FIRST stage of the run of BMO_1 whose centre contains the strict transform c̃ of a component c of V(I) along which I is reduced. The rounds of Step 1 of the proof of [Kol07, Theorem 107] at an order d ≥ 2 blow up centres along which the nonmonomial part has order ≥ d; such a centre cannot contain c̃: at the generic point η̃ of c̃ the nonmonomial part is the maximal ideal, of order 1 (ord_maximalIdeal_eq_one), and the order at η̃ is at least the order at a generic point of the centre specializing to it (upper semicontinuity of the order, [Hau03, p. 392]). So the first containing stage lies in the round of order 1. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimStep1, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedGenericOrder and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step1.

theorem Hironaka.Resolution.notMem_of_leOrdAlong_two {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (D : TopologicalSpace.Closeds ↥X) (hD : I.LeOrdAlong D ↑2) {η : ↥X} (hη : I.ord η ≤ 1) : η ∉ D

A point at which an ideal sheaf has order 1 lies on no closed set along which the ideal sheaf has order ≥ 2 (the order at a specialization is at least the order at the generic point); the order at the point may be ≤ 1.

theorem Hironaka.Resolution.not_centerContains_of_leOrdAlong_two {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (hS : S.IsSmooth f) (c : X.IdealSheafData) (i : Fin S.length) (N : (S.stage i.castSucc).IdealSheafData) (hN : N.LeOrdAlong (S.center i).support ↑2) {η : ↥(S.stage i.castSucc)} (hη : η ∈ (S.strictTransformSeq c i.castSucc).support) (hord : N.ord η ≤ 1) : ¬CenterContains S c ↑i

Step 1 of the proof of [Kol07, Theorem 107] read against the Claim: a centre along which the marked ideal has order ≥ 2 does not contain the strict transform of a component whose generic point carries order ≤ 1. The run is smooth (S.IsSmooth f), so its stages are smooth of relative dimension n over k and the semicontinuity applies at stage i.