CP1 at the absorbing stage of the loop

The loop bedAux of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.Embedded) truncates the run of BMO_1 before its first absorbing blow-up, the stage Nat.find h at which some member c ∈ C has its strict transform contained in the centre. For such a member, the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) along the run (cp1For_bmoOneRun_of_cp1BMOAt, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Tower) gives the chain form of the marked transform along the strict transform c̃ at that stage; carried to the last stage of the truncation (whose data are those of the run at that stage), this is chainRelativeAt_of_absorbed_of_cp1For. And the chain form forces the strict transforms of the other members off c̃ at that stage (disjoint_strictTransformSeq_of_absorbed_of_chainRelativeAt): at a common point p, the prime (c̃')_p contains I_p = M⁰ · chainIdeal and none of the monomials (the lifted generic points of the members lie on no member of the boundary), hence every chain equation (span_range_le_of_mul_chainIdeal_le_prime), hence (c̃)_p; so the generic point of c̃' lies on c̃, and both being generic points of V(I) at that stage (the proof of Kol07, Corollary 22) they coincide, giving c' = c (eq_of_strictTransformSeq_eq). This is the absorbing moment of the proof of [Wlo05, Theorem 4.7.1], with the chain form in place of Włodarczyk's Claim. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Main.

Bookkeeping across the truncation's stage identification

theorem Hironaka.Resolution.heq_support {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {I : Y.IdealSheafData} {I' : Y'.IdealSheafData} (hI : I ≍ I') : I.support ≍ I'.support

Heterogeneous equality of ideal sheaves gives heterogeneous equality of their supports.

theorem Hironaka.Resolution.disjoint_of_heq {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {A B : TopologicalSpace.Closeds ↥Y} {A' B' : TopologicalSpace.Closeds ↥Y'} (hA : A ≍ A') (hB : B ≍ B') (hd : Disjoint A' B') : Disjoint A B

Disjointness of closed sets transports across an equality of schemes.

theorem Hironaka.Resolution.chainRelativeAt_of_absorbed_of_cp1For {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)) (hcp : ∀ η ∈ T.I.support.genericPoints, (∀ (i : T.E.ι), η ∉ (T.E.component i).support) → T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η → CP1For (bmoOneRun T hm) T.I T.E η) (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

From CP1 along bmoOneRun for the generic points of the members to the chain form at the absorbing stage of the loop: Nat.find h is the first containing index, and the data of the truncation at its last stage are the data of the run at that stage.

theorem Hironaka.Resolution.disjoint_strictTransformSeq_of_absorbed_of_chainRelativeAt {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)) (hloc : ∀ 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) {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

The disjointness of the other members from the absorbed one, from the local chain form at every point of the strict transform c̃ of the absorbed member: at a common point p the prime (c̃')_p ⊇ I_p = M⁰ · chainIdeal with the monomials not in the prime (the lifted generic point of c' lies on no member of the boundary) contains the equations of the chain, hence (c̃)_p, so the generic point of c̃' lies on c̃; both are generic points of V(I) at that stage (the proof of [Kol07, Corollary 22]), so they coincide and c' = c.