The isolated state is protected for the absorbed member

At the first absorbing stage Nat.find h of the loop, the strict transform Γ = c̃ of an absorbed member is: smooth over k and integral (the stalks of the centre are those of Γ at every point of Γ, stalkIdeal_center_eq_strictTransformSeq_of_first of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFirstCenterEq, and the centre has simple normal crossings with the boundary by clause (3′) of [Kol07, Definition 66], so Γ has snc and is smooth; integrality by isIntegral_strictTransformSeq_of_le_firstCenterIndex); disjoint from the strict transforms of the remaining members (CP1, disjoint_strictTransformSeq_of_absorbed); and the isolated ideal I_n : I_Γ has the K-shape along Γ (CP1 gives the chain form of I_n, CP2 chainRelativeKAt_colon of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainColon the K-shape of the colon by Γ, and at a point of Γ the reduced ideal I_Γ of the absorbed strict transforms has the stalk of Γ, the absorbed strict transforms being integral and pairwise disjoint by CP1). This is protectedState_isolatedTriple_of_absorbed, the entry into the invariant CP5 (ProtectedState, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative). It replaces, without the false hypothesis ClaimKC, the isolation step of the proof of [Wlo05, Theorem 4.7.1]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Isolation, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCPBridge.

Bookkeeping

theorem Hironaka.Resolution.chainRelativeKAt_congr_stalkIdeal_K {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {K K' Γ : X.IdealSheafData} {p : ↥X} (h : K.stalkIdeal p = K'.stalkIdeal p) : ChainRelativeKAt E K Γ p ↔ ChainRelativeKAt E K' Γ p

The K-shape depends on K only through its stalk at p.

theorem Hironaka.Resolution.isIntegral_of_heq {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {I : Y.IdealSheafData} {I' : Y'.IdealSheafData} (hI : I ≍ I') (hint : AlgebraicGeometry.IsIntegral I'.subscheme) : AlgebraicGeometry.IsIntegral I.subscheme

Integrality of the closed subscheme transports across an equality of schemes.

theorem Hironaka.Resolution.hasSncWith_strictTransformSeq_of_first {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} (hS : S.IsOrderGeSeq f I 1 E) {η : ↥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) : (S.totalTransformSeq E j.castSucc).HasSncWith (S.strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) j.castSucc)

The strict transform of c̄ has simple normal crossings with the boundary at a stage whose centre contains it while no earlier centre does (clause (c) of [Wlo05, Theorem 1.0.2] at a first containing stage; the unconditional form of hasSncWith_strictTransformSeq_of_absorbed): [Kol07, Definition 24 (4)] read at its points, where its stalks are those of the centre (stalkIdeal_center_eq_strictTransformSeq_of_first) and the centre has snc with the boundary ([Kol07, Definition 66 (3′)]).

theorem Hironaka.Resolution.isIntegral_take_strictTransformSeq_of_mem {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) {c : T.X.left.IdealSheafData} (hc : c ∈ C) : AlgebraicGeometry.IsIntegral (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).subscheme

At the loop's stage, the truncated strict transform of every member is integral (no centre before the stage contains it, isIntegral_strictTransformSeq_of_le_firstCenterIndex).

theorem Hironaka.Resolution.pairwise_disjoint_take_strictTransformSeq_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : (↑({c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)})).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq a (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq b (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support

The truncated strict transforms of the members absorbed at the stage of the loop are pairwise disjoint (CP1).

theorem Hironaka.Resolution.stalkIdeal_vanishingIdeal_absorbed_of_mem {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) {c : T.X.left.IdealSheafData} (hcC : c ∈ C) (hcc : CenterContains (bmoOneRun T hm) c (Nat.find h)) {p : ↥(((bmoOneRun T hm).take (Nat.find h)).stage (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length))} (hp : p ∈ (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (⨆ c' ∈ {c' ∈ C | CenterContains (bmoOneRun T hm) c' (Nat.find h)}, (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c' (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support)).stalkIdeal p = (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).stalkIdeal p

At a point of an absorbed member's truncated strict transform Γ, the reduced ideal of the union of the absorbed strict transforms has Γ's stalk (integral, pairwise disjoint).

theorem Hironaka.Resolution.protectedState_isolatedTriple_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (hinv : InvCE T.I T.E C) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) {c : T.X.left.IdealSheafData} (hcC : c ∈ C) (hcc : CenterContains (bmoOneRun T hm) c (Nat.find h)) : ProtectedState (isolatedTriple T hm C (Nat.find h)) (remainingComponents T hm C (Nat.find h)) (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length))

The entry into the protected state: the isolated state at the first absorbing stage of the loop is protected for the absorbed member — its strict transform is smooth and integral, has snc with the boundary, misses the strict transforms of the remaining members, and the isolated ideal has the K-shape along it.