At the absorbing stage: the centre is the strict transform, under Włodarczyk's Claim

In the proof of [Wlo05, Theorem 4.7.1], at the moment the strict transform Ỹ₁ of a component is the centre, the controlled transform of I has order 1 along Ỹ₁ and is its ideal near Ỹ₁ — Włodarczyk's Claim. In Kollár's setting it is the proposition ClaimKC (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses): at the first stage n whose centre D contains the strict transform c̃ of a member c, the nonmonomial part N(I_n) of the marked ideal agrees with c̃ at every point of c̃. ClaimKC fails for the order of the steps of BMO_1 used here (see that module); this module draws, CONDITIONALLY on it, the consequences the loop would need. The unconditional replacements are proved from the local form of the ideal (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry: the strict transform of an absorbed member is smooth, integral, with simple normal crossings with the boundary, and disjoint from the other members).

• stalkIdeal_center_eq_of_absorbed — at every point p of c̃, D_p = c̃_p: D ≤ c̃ by the stop rule; conversely I_n ≤ D (the centre lies in the cosupport, [Kol07, Definition 66 (4′)]), I_n = M(I_n) · N(I_n) (the splitting of [Kol07, Definition–Lemma 110]) and N(I_n)_p = c̃_p (Włodarczyk's Claim), so M(I_n)_p · c̃_p ≤ D_p with D_p PRIME (the centre is smooth, 𝒪_p / D_p a regular local ring, a domain); M(I_n)_p ⊄ D_p since a piece of the boundary containing D near p would contain the generic point of c̃, which lies on no member of the boundary.
• hasSncWith_strictTransformSeq_of_absorbed, smooth_strictTransformSeq_of_absorbed — c̃ has simple normal crossings with the boundary at stage n and is smooth: [Kol07, Definition 24 (4)] is read at the points of c̃, where c̃ has the stalks of the centre, which has snc with the boundary ([Kol07, Definition 66 (3′)]); smoothness by HasSncWith.smooth.
• stalkIdeal_markedTransformSeq_eq_mul_of_absorbed — I_n = M(I_n) · I_c̃ at the points of c̃ (Włodarczyk's σ^c(I) = I_Ỹ₁ with the monomial part).

All statements are at the run's stage n.castSucc (the index form). The unconditional lemmas of the first section (val_le_firstCenterIndex_of_absorbed, exists_genericPoint_strictTransformSeq_of_absorbed, markedTransformSeq_le_center_of_absorbed) are stated without the hypothesis ClaimKC and are used elsewhere.

The data of an absorbed member: T a marked triple of mark 1, η the generic point of a component of V(T.I) lying on no member of the boundary at which T.I agrees with the component's reduced ideal c, and n the FIRST centre index of the run whose centre contains the strict transform of c.

theorem Hironaka.Resolution.val_le_firstCenterIndex_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {η : ↥T.X.left} (n : Fin (bmoOneRun T hm).length) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) : ↑n ≤ firstCenterIndex (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η}))

The stage n is at most the first containing index of the member.

theorem Hironaka.Resolution.exists_genericPoint_strictTransformSeq_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {η : ↥T.X.left} (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (n : Fin (bmoOneRun T hm).length) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) : ∃ (η' : ↥((bmoOneRun T hm).stage n.castSucc)), IsGenericPoint η' ↑((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).support ∧ ((bmoOneRun T hm).stageMap n.castSucc) η' = η ∧ (∀ (y : ↥((bmoOneRun T hm).stage n.castSucc)), ((bmoOneRun T hm).stageMap n.castSucc) y = η → y = η') ∧ (∀ (m : Fin (bmoOneRun T hm).length) (hmi : ↑m < ↑n.castSucc), ((bmoOneRun T hm).stageMapBetween n.castSucc m.castSucc ⋯) η' ∉ ((bmoOneRun T hm).center m).support) ∧ CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap ((bmoOneRun T hm).stageMap n.castSucc) η') ∧ ∀ (i : ((bmoOneRun T hm).totalTransformSeq T.E n.castSucc).ι), η' ∉ (((bmoOneRun T hm).totalTransformSeq T.E n.castSucc).component i).support

The proof of [Kol07, Corollary 22] for the absorbed member: the strict transform c̃ at stage n has a generic point η', the unique point over η, transported by isomorphisms of stalks and lying on no member of the boundary at stage n.

The centre agrees with the strict transform at its points (K2a)

theorem Hironaka.Resolution.not_monomialPart_stalkIdeal_le_center_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {η : ↥T.X.left} (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (n : Fin (bmoOneRun T hm).length) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) {p : ↥((bmoOneRun T hm).stage n.castSucc)} (hp : p ∈ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).support) (hprime : (((bmoOneRun T hm).center n).stalkIdeal p).IsPrime) (hDle : (bmoOneRun T hm).center n ≤ (bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc) : ¬(BMO.monomialPart ((bmoOneRun T hm).markedTransformSeq T.I 1 n.castSucc) ((bmoOneRun T hm).totalTransformSeq T.E n.castSucc)).stalkIdeal p ≤ ((bmoOneRun T hm).center n).stalkIdeal p

The fine monomial part of the marked ideal at the absorbing stage is not contained in the centre's stalk at a point of the absorbed strict transform: a piece of the boundary containing the centre near p would, by generization to the generic point η' of the strict transform, contain η' — which lies on no member of the boundary.

theorem Hironaka.Resolution.markedTransformSeq_le_center_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (n : Fin (bmoOneRun T hm).length) : (bmoOneRun T hm).markedTransformSeq T.I 1 n.castSucc ≤ (bmoOneRun T hm).center n

[Kol07, Definition 66 (4′)]: the marked ideal at the absorbing stage is contained in the centre's ideal — the centre lies in the cosupport (order ≥ 1 at its generic points), and the centre is reduced (smooth).

theorem Hironaka.Resolution.stalkIdeal_center_eq_of_absorbed {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 η) (n : Fin (bmoOneRun T hm).length) (habs : CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ↑n) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) (hKC : ClaimKC k) {p : ↥((bmoOneRun T hm).stage n.castSucc)} (hp : p ∈ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).support) : ((bmoOneRun T hm).center n).stalkIdeal p = ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).stalkIdeal p

Under the hypothesis ClaimKC (Włodarczyk's Claim; false for the transcribed order): at every point p of the absorbed strict transform c̃, the centre's stalk is c̃'s — D ≤ c̃ by the stop rule; conversely I_n ≤ D, I_n = M(I_n) · N(I_n) and N(I_n)_p = c̃_p (Włodarczyk's Claim) give M(I_n)_p · c̃_p ≤ D_p, D_p is prime, and M(I_n)_p ⊄ D_p.

K2, K1, K3

theorem Hironaka.Resolution.hasSncWith_strictTransformSeq_of_absorbed {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 η) (n : Fin (bmoOneRun T hm).length) (habs : CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ↑n) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) (hKC : ClaimKC k) : ((bmoOneRun T hm).totalTransformSeq T.E n.castSucc).HasSncWith ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc)

Under the hypothesis ClaimKC: the absorbed strict transform has simple normal crossings with the boundary at stage n — [Kol07, Definition 24 (4)] read at its points, where its stalks are the centre's (stalkIdeal_center_eq_of_absorbed) and the centre has snc with the boundary ([Kol07, Definition 66 (3′)]). The unconditional form is in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry.

theorem Hironaka.Resolution.smooth_strictTransformSeq_of_absorbed {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 η) (n : Fin (bmoOneRun T hm).length) (habs : CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ↑n) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) (hKC : ClaimKC k) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).subschemeι (CategoryTheory.CategoryStruct.comp ((bmoOneRun T hm).stageMap n.castSucc) (T.X.left ↘ AlgebraicGeometry.Spec ↧k)))

Under the hypothesis ClaimKC: the absorbed strict transform is smooth over k (HasSncWith.smooth). The unconditional form is in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry.

theorem Hironaka.Resolution.stalkIdeal_markedTransformSeq_eq_mul_of_absorbed {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 η) (n : Fin (bmoOneRun T hm).length) (habs : CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ↑n) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) (hKC : ClaimKC k) {p : ↥((bmoOneRun T hm).stage n.castSucc)} (hp : p ∈ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).support) : ((bmoOneRun T hm).markedTransformSeq T.I 1 n.castSucc).stalkIdeal p = (BMO.monomialPart ((bmoOneRun T hm).markedTransformSeq T.I 1 n.castSucc) ((bmoOneRun T hm).totalTransformSeq T.E n.castSucc)).stalkIdeal p * ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).stalkIdeal p

Under the hypothesis ClaimKC: at every point of the absorbed strict transform, the marked ideal is the monomial part times the strict transform's ideal (Włodarczyk's Claim with the monomial part of [Kol07, Definition–Lemma 110]).