CP1 at the absorbing stage: the two statements

The two forms of the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) at the absorbing stage of the loop, as compositions: the local chain form (chainRelativeAt_of_absorbed, which is chainRelativeAt_of_absorbed_of_cp1For applied to cp1For_bmoOneRun_of_cp1BMOAt and cp1BMOAt) and the disjointness of the strict transforms of the other members from the absorbed one there (disjoint_strictTransformSeq_of_absorbed, which is disjoint_strictTransformSeq_of_absorbed_of_chainRelativeAt at the former). These are the inputs of the entry into the protected state (CP2, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry), of the invariant CP5 and of the end identity CP6. The absorbing moment is that of the proof of [Wlo05, Theorem 4.7.1]; the tower induction behind cp1BMOAt is that of [Kol07, 70].

theorem Hironaka.Resolution.chainRelativeAt_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)) (p : ↥(((bmoOneRun T hm).take (Nat.find h)).stage (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length))) : p ∈ (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support → ChainRelativeAt (stageTriple T hm (Nat.find h)).E (stageTriple T hm (Nat.find h)).I (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) p

CP1, the local form at the absorbing stage of the loop: at the first absorbing stage of the run of BMO_1 on a state of the loop, the marked transform is in chain form along the strict transform of the absorbed member at every point of it.

theorem Hironaka.Resolution.disjoint_strictTransformSeq_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)) {c' : T.X.left.IdealSheafData} (hc'C : c' ∈ C) (hne : c' ≠ c) : Disjoint (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c' (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).support

CP1, the disjointness: no other member's strict transform meets the absorbed one at the absorbing stage.