CP5: the protected state through the run, the truncations, the isolations and the loop

The statement CP5 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): once a component is absorbed and isolated, the loop keeps its strict transform Γ̃ smooth, integral, snc with the boundary and off the other members, and keeps the isolated ideal in the K-shape along it; at the end the isolated ideal is trivial near Γ̃_end.

• The round (protectedData_seq, protectedData_blowUp): along a smooth sequence of order ≥ 1 whose centres are classified at their points (CP3, cp3For_bmoOneRun), each blow-up is along an admissible chain stratum at the points of Γ̃ (admissibleChainStratumKAt_of_centerClassifiedAt, the K-shape read in its own chain coordinates), so CP4 (chainRelativeKAt_strictTransform) gives the snc and the K-shape after the blow-up; the strict transform stays integral because an admissible stratum never contains Γ̃ (not_le_of_admissibleChainStratumKAt: the condition (★) forces a member's coordinate into the ideal of the stratum, which the span of the chain does not contain) and stays off the strict transforms of the members (disjoint_strictTransform_support_of_disjoint).
• The truncation (protectedState_stageTriple) reads the data of the run at the stage n on the truncated run (stage_take_last and the casts of the truncation); the classification of the centres of a run on a protected state (admissibleChainStratumKAt_center_of_protectedState) is CP3 at a stage.
• The isolation (protectedState_isolatedTriple): the strict transforms of the absorbed members miss Γ̃, so the colon by their reduced ideal has the stalk of K at every point of Γ̃ (stalkIdeal_isolatedTriple_I_eq_of_protectedState, stalkIdeal_colon_eq_of_notMem_support).
• The last round (stalkIdeal_markedTransformSeq_bmoOneRun_last_eq_top, [Kol07, Theorem 69 (1)]): the untruncated run ends with max-ord < 1, the unit ideal at every point (the stalk form of markedTransformSeq_bmoOneRun_last_eq_top).
• The loop (protected_bedAux): strong induction on the number of members along bedAux (bedAux_of_exists, bedAux_of_not_exists); the data of the concatenation are read through the casts (last_concat, strictTransformSeq_concat_last_heq, composite_concat), and the transform of the ideal of the state along the rest of the loop agrees with that of the isolated ideal at the points of Γ̃ (stalkIdeal_markedTransformSeq_eq_of_forall_stalkIdeal_eq, the locality of the marked transform iterated).

This is the isolation passage of the proof of [Wlo05, Theorem 4.7.1] ("ignoring these isolated components"), proved from CP3 and CP4 in place of Włodarczyk's invariant; the argument is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCPBridge.

theorem Hironaka.Resolution.smooth_subschemeι_comp_of_heq_map {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {Γ : Y.IdealSheafData} {Γ' : Y'.IdealSheafData} (hΓ : Γ ≍ Γ') {W : AlgebraicGeometry.Scheme} {g : Y ⟶ W} {g' : Y' ⟶ W} (hg : g ≍ g') (hs : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Γ'.subschemeι g')) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Γ.subschemeι g)

Smoothness of a closed subscheme over a base transports across a cast of the ambient scheme, the structure map carried whole.

theorem Hironaka.Resolution.forall_stalkIdeal_eq_top_of_heq {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {Γ M : Y.IdealSheafData} {Γ' M' : Y'.IdealSheafData} (hΓ : Γ ≍ Γ') (hM : M ≍ M') (hs : ∀ p ∈ Γ'.support, M'.stalkIdeal p = ⊤) (p : ↥Y) : p ∈ Γ.support → M.stalkIdeal p = ⊤

"The unit stalk at every point of a closed subscheme" transports across a cast.

theorem Hironaka.Resolution.heq_eqToHom_comp {Y Y' Z : AlgebraicGeometry.Scheme} (e : Y = Y') (φ : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e) φ ≍ φ

A cast composed with a morphism is heterogeneously the morphism.

The one-blow-up step and the run

theorem Hironaka.Resolution.admissibleChainStratumKAt_of_centerClassifiedAt {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {K Γ Z : X.IdealSheafData} {p : ↥X} (hK : ChainRelativeKAt E K Γ p) (hcl : CenterClassifiedAt E K Z p) : AdmissibleChainStratumKAt E K Γ Z p

At a point of the centre on the protected component, the classification of the centre (CP3) in the chain coordinates of the K-shape is admissibility.

theorem Hironaka.Resolution.not_le_of_admissibleChainStratumKAt {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {K Γ Z : X.IdealSheafData} {p : ↥X} [IsRegularLocalRing ↑(X.presheaf.stalk p)] (h : AdmissibleChainStratumKAt E K Γ Z p) : ¬Z ≤ Γ

An admissible chain stratum at a point of Γ does not contain Γ (as ideal sheaves): the condition (★) puts a member's coordinate z k, k ∈ s, into its stalk, and that coordinate lies outside the span of the chain.

theorem Hironaka.Resolution.protectedData_blowUp {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (K Γ Z : X.IdealSheafData) (C : Set X.IdealSheafData) (hE : E.IsSnc) (hΓ : E.HasSncWith Γ) (hint : AlgebraicGeometry.IsIntegral Γ.subscheme) (hdisj : ∀ c ∈ C, Disjoint c.support Γ.support) (hK : ∀ p ∈ Γ.support, ChainRelativeKAt E K Γ p) (hcl : ∀ q ∈ Z.support, CenterClassifiedAt E K Z q) : (E.totalTransform Z).HasSncWith (Γ.strictTransform Z) ∧ AlgebraicGeometry.IsIntegral (Γ.strictTransform Z).subscheme ∧ (∀ c ∈ C, Disjoint (c.strictTransform Z).support (Γ.strictTransform Z).support) ∧ ∀ q ∈ (Γ.strictTransform Z).support, ChainRelativeKAt (E.totalTransform Z) (K.markedTransform Z 1) (Γ.strictTransform Z) q

One blow-up of a protected state (CP3 with CP4): along the blow-up of a centre classified at each of its points, the strict transform of Γ stays snc with the boundary, integral and disjoint from the strict transforms of the members, and the transform of K keeps the K-shape along it.

theorem Hironaka.Resolution.protectedData_seq {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (E : X.DivisorFamily) (K Γ : X.IdealSheafData) (C : Set X.IdealSheafData) : S.IsOrderGeSeq f K 1 E → CP3For S K E → E.IsSnc → E.HasSncWith Γ → AlgebraicGeometry.IsIntegral Γ.subscheme → (∀ c ∈ C, Disjoint c.support Γ.support) → (∀ p ∈ Γ.support, ChainRelativeKAt E K Γ p) → ∀ (i : Fin (S.length + 1)), (S.totalTransformSeq E i).HasSncWith (S.strictTransformSeq Γ i) ∧ AlgebraicGeometry.IsIntegral (S.strictTransformSeq Γ i).subscheme ∧ (∀ c ∈ C, Disjoint (S.strictTransformSeq c i).support (S.strictTransformSeq Γ i).support) ∧ ∀ p ∈ (S.strictTransformSeq Γ i).support, ChainRelativeKAt (S.totalTransformSeq E i) (S.markedTransformSeq K 1 i) (S.strictTransformSeq Γ i) p

The protected data along a run, stage by stage: along a smooth sequence of order ≥ 1 for (K, 1) whose centres are classified at each of their points (CP3), from a protected input — Γ snc with the boundary, integral, disjoint from the members C, K in the K-shape along it — the strict transform of Γ at every stage is snc with the total transform of the boundary, integral and disjoint from the strict transforms of the members, and the mark-1 transform of K keeps the K-shape along it.

theorem Hironaka.Resolution.stalkIdeal_markedTransformSeq_eq_of_forall_stalkIdeal_eq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (I K Γ : X.IdealSheafData) : (∀ p ∈ Γ.support, I.stalkIdeal p = K.stalkIdeal p) → ∀ (i : Fin (S.length + 1)), ∀ q ∈ (S.strictTransformSeq Γ i).support, (S.markedTransformSeq I 1 i).stalkIdeal q = (S.markedTransformSeq K 1 i).stalkIdeal q

The locality of the marked transform iterated: two ideals with the same stalks at every point of Γ have mark-1 transforms with the same stalks at every point of the strict transform of Γ, at every stage (the strict transform lies over Γ; the stalk of the transform at a point depends only on the stalk of the ideal at its image).

The protected state along the loop

theorem Hironaka.Resolution.protectedData_bmoOneRun {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (Γ : T.X.left.IdealSheafData) (hP : ProtectedState T C Γ) (i : Fin ((bmoOneRun T hm).length + 1)) : ((bmoOneRun T hm).totalTransformSeq T.E i).HasSncWith ((bmoOneRun T hm).strictTransformSeq Γ i) ∧ AlgebraicGeometry.IsIntegral ((bmoOneRun T hm).strictTransformSeq Γ i).subscheme ∧ (∀ c ∈ C, Disjoint ((bmoOneRun T hm).strictTransformSeq c i).support ((bmoOneRun T hm).strictTransformSeq Γ i).support) ∧ ∀ p ∈ ((bmoOneRun T hm).strictTransformSeq Γ i).support, ChainRelativeKAt ((bmoOneRun T hm).totalTransformSeq T.E i) ((bmoOneRun T hm).markedTransformSeq T.I 1 i) ((bmoOneRun T hm).strictTransformSeq Γ i) p

The data of the run at every stage of bmoOneRun, from a protected state: protectedData_seq with cp3For_bmoOneRun.

theorem Hironaka.Resolution.admissibleChainStratumKAt_center_of_protectedState {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (Γ : T.X.left.IdealSheafData) (hP : ProtectedState T C Γ) (i : Fin (bmoOneRun T hm).length) (p : ↥((bmoOneRun T hm).stage i.castSucc)) : p ∈ ((bmoOneRun T hm).center i).support ⊓ ((bmoOneRun T hm).strictTransformSeq Γ i.castSucc).support → AdmissibleChainStratumKAt ((bmoOneRun T hm).totalTransformSeq T.E i.castSucc) ((bmoOneRun T hm).markedTransformSeq T.I 1 i.castSucc) ((bmoOneRun T hm).strictTransformSeq Γ i.castSucc) ((bmoOneRun T hm).center i) p

The centres of a run on a protected state are admissible chain strata (CP3 at a stage): every centre meeting the protected component is an ADMISSIBLE chain stratum for the isolated ideal of the run — the stratum, the K-shape and (★) in shared chain coordinates.

theorem Hironaka.Resolution.protectedState_stageTriple {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (Γ : T.X.left.IdealSheafData) (hP : ProtectedState T C Γ) (n : ℕ) (hn : n ≤ (bmoOneRun T hm).length) : ProtectedState (stageTriple T hm n) (transportedComponents T hm C n) (((bmoOneRun T hm).take n).strictTransformSeq Γ (Fin.last ((bmoOneRun T hm).take n).length))

The round lemma (CP3 with CP4): the protected state persists along the run truncated anywhere (the isolation passage of the proof of [Wlo05, Theorem 4.7.1]).

theorem Hironaka.Resolution.stalkIdeal_colon_eq_of_notMem_support {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (I K : X.IdealSheafData) {p : ↥X} (hp : p ∉ K.support) : (I.colon K).stalkIdeal p = I.stalkIdeal p

The stalk of a colon at a point off the support of the divisor is the stalk of the ideal (stalkIdeal_colon_of_isLocallyNoetherian, the colon by the unit ideal).

theorem Hironaka.Resolution.stalkIdeal_isolatedTriple_I_eq_of_protectedState {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (Γ : T.X.left.IdealSheafData) (n : ℕ) (hP : ProtectedState (stageTriple T hm n) (transportedComponents T hm C n) (((bmoOneRun T hm).take n).strictTransformSeq Γ (Fin.last ((bmoOneRun T hm).take n).length))) {p : ↥(((bmoOneRun T hm).take n).stage (Fin.last ((bmoOneRun T hm).take n).length))} (hp : p ∈ (((bmoOneRun T hm).take n).strictTransformSeq Γ (Fin.last ((bmoOneRun T hm).take n).length)).support) : (isolatedTriple T hm C n).I.stalkIdeal p = (stageTriple T hm n).I.stalkIdeal p

The isolation is the identity near Γ̃: at a point of the strict transform of the protected component, the isolated ideal has the stalk of the ideal of the stage — the strict transforms of the absorbed members miss Γ̃, so the reduced ideal of their union has the unit stalk there.

theorem Hironaka.Resolution.protectedState_isolatedTriple {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (Γ : T.X.left.IdealSheafData) (hP : ProtectedState T C Γ) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : ProtectedState (isolatedTriple T hm C (Nat.find h)) (remainingComponents T hm C (Nat.find h)) (((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq Γ (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length))

The isolation lemma: the protected state passes through the isolation of the loop (the isolation passage of the proof of [Wlo05, Theorem 4.7.1]).

theorem Hironaka.Resolution.stalkIdeal_markedTransformSeq_bmoOneRun_last_eq_top {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (p : ↥(bmoOneRun T hm).last) : ((bmoOneRun T hm).markedTransformSeq T.I 1 (Fin.last (bmoOneRun T hm).length)).stalkIdeal p = ⊤

The last-round lemma ([Kol07, Theorem 69 (1)]): the untruncated run of BMO_1 ends with the ideal trivial at EVERY point — max-ord < 1 means order 0 everywhere — the stalk form of markedTransformSeq_bmoOneRun_last_eq_top.

theorem Hironaka.Resolution.protected_bedAux {k : Type u} [Field k] [CharZero k] (N : ℕ) (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (Γ : T.X.left.IdealSheafData) : C.card = N → ProtectedState T C Γ → AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp ((bedAux T hm C).strictTransformSeq Γ (Fin.last (bedAux T hm C).length)).subschemeι (CategoryTheory.CategoryStruct.comp (bedAux T hm C).composite (T.X.left ↘ AlgebraicGeometry.Spec ↧k))) ∧ ((bedAux T hm C).totalTransformSeq T.E (Fin.last (bedAux T hm C).length)).HasSncWith ((bedAux T hm C).strictTransformSeq Γ (Fin.last (bedAux T hm C).length)) ∧ ∀ p ∈ ((bedAux T hm C).strictTransformSeq Γ (Fin.last (bedAux T hm C).length)).support, ((bedAux T hm C).markedTransformSeq T.I 1 (Fin.last (bedAux T hm C).length)).stalkIdeal p = ⊤

The loop theorem, CP5: strong induction on C.card — from a protected state, the loop ends with the component smooth, snc with the boundary, and the isolated ideal trivial along it (the proof of [Wlo05, Theorem 4.7.1]).