The loop of the un-isolated ideal

The statement CP6 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) follows the un-isolated ideal I₀ = I_A ⊓ K — the controlled transform of I_Y along the WHOLE loop bedAux of Hironaka.Resolution.Algebraic.Wlo05.Embedded, isolations ignored — and proves the end identity: at the end of the loop the transform of I_Y is the product of the final strict transforms of the members, which are pairwise disjoint (the marked_eq and pairwise clauses of the end data of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedState, hence the fine form of clause (e) of Wlo05, Theorem 1.0.2). This module proves that argument on bedAux, bmoOneRun, stageTriple, isolatedTriple and remainingComponents:

• the FULL-RUN form of the intersection form along a round, bmoOneRun_marked_eq_inf_of_protectedStates — the per-stage engine markedTransformSeq_eq_biInf_inf_of_forall_stage (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Stage) on the run of BMO_1, its hypotheses supplied by the protected states of CP5 (protectedState_stageTriple through the casts of the truncation, admissibleChainStratumKAt_center_of_protectedState), the order property of the run (smooth stages, snc boundary) and K_i ≤ Z_i (markedTransformSeq_le_center_of_isOrderGeSeq); its truncated form is markedTransformSeq_take_eq_inf_of_protectedStates;
• the isolation step isolatedTriple_marked_eq_inf_of_absorbed — the truncated form at the absorbing stage with the isolation identity markedTransformSeq_take_eq_biInf_inf_colon (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Isolation): the invariant is re-established with the enlarged protected set and the isolated ideal;
• protectedState_transported_of_absorbed — the enlarged protected set is protected for the isolated state (CP5's protectedState_isolatedTriple for the transports, the entry of CP2 for the absorbed members);
• the loop theorem bedAux_marked_eq_biInf_of_protectedStates and the loop separates bedAux_pairwise_disjoint_of_protectedStates — strong induction on the number of members along bedAux_of_exists and bedAux_of_not_exists: at an absorbing stage the goal transports across the concatenation, the isolation step and the transported protected set feed the induction hypothesis at the isolated triple (with invCE_isolatedTriple, card_remainingComponents_lt), the index sets match membership-wise; with no absorption the members are empty by exhaustiveness and the full-run form at the end with markedTransformSeq_bmoOneRun_last_eq_top closes;
• the end identity markedTransformSeq_bedAux_last_eq_prod: both clauses at Γs = ∅, the product from the meet by prod_eq_inf_of_pairwise_disjoint, stated for every state satisfying InvCE.

This is the identity σ^*(I_Y) = M(σ^*(I_Y)) · I_Ỹ of [Wlo05, Theorem 4.7.1] up to the monomial factor, proved from the chain forms; the argument is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCPBridge and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Remaining.

theorem Hironaka.Resolution.bmoOneRun_marked_eq_inf_of_protectedStates {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C Γs : Finset T.X.left.IdealSheafData) (I₀ : T.X.left.IdealSheafData) (hP : ∀ γ ∈ Γs, ProtectedState T C γ) (hdisj : (↑Γs).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint a.support b.support) (hI₀ : I₀ = (⨅ γ ∈ Γs, γ) ⊓ T.I) (i : Fin ((bmoOneRun T hm).length + 1)) : (bmoOneRun T hm).markedTransformSeq I₀ 1 i = (⨅ γ ∈ Γs, (bmoOneRun T hm).strictTransformSeq γ i) ⊓ (bmoOneRun T hm).markedTransformSeq T.I 1 i

The full-run form of the intersection form along a round: from a state with pairwise disjoint protected components Γs, the transform of I₀ = (⨅ γ ∈ Γs, γ) ⊓ T.I at every stage of the run is the meet of the transported protected components with the transform of T.I — markedTransformSeq_eq_biInf_inf_of_forall_stage on bmoOneRun T hm, its per-stage hypotheses supplied by the protected states of CP5 (protectedState_stageTriple through the casts of the truncation, and admissibleChainStratumKAt_center_of_protectedState), the order property of the run (snc boundary, smooth stages, K_i ≤ Z_i by markedTransformSeq_le_center_of_isOrderGeSeq) and the integrality of the members (reducedness).

theorem Hironaka.Resolution.markedTransformSeq_take_eq_inf_of_protectedStates {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C Γs : Finset T.X.left.IdealSheafData) (I₀ : T.X.left.IdealSheafData) (hP : ∀ γ ∈ Γs, ProtectedState T C γ) (hdisj : (↑Γs).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint a.support b.support) (hI₀ : I₀ = (⨅ γ ∈ Γs, γ) ⊓ T.I) (n : ℕ) (hn : n ≤ (bmoOneRun T hm).length) : ((bmoOneRun T hm).take n).markedTransformSeq I₀ 1 (Fin.last ((bmoOneRun T hm).take n).length) = (⨅ γ ∈ Γs, ((bmoOneRun T hm).take n).strictTransformSeq γ (Fin.last ((bmoOneRun T hm).take n).length)) ⊓ ((bmoOneRun T hm).take n).markedTransformSeq T.I 1 (Fin.last ((bmoOneRun T hm).take n).length)

The intersection form along a round, truncated anywhere: from the start of a round with the protected members Γs (each a protected state, pairwise disjoint supports) and the un-isolated ideal I₀ = (⨅ γ ∈ Γs, γ) ⊓ T.I, the identity persists along the run truncated anywhere — markedTransform_inf_of_admissible iterated with CP3 for the centres. Off the Γ̃ it reads I_n = K_n; at their points it is the local un-isolated form.

theorem Hironaka.Resolution.protectedState_transported_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) (Γs : Finset T.X.left.IdealSheafData) (hP : ∀ γ ∈ Γs, ProtectedState T C γ) (γ' : (((bmoOneRun T hm).take (Nat.find h)).stage (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)).IdealSheafData) : γ' ∈ Finset.image (fun (γ : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq γ (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) Γs ∪ Finset.image (fun (c : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) ({c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}) → ProtectedState (isolatedTriple T hm C (Nat.find h)) (remainingComponents T hm C (Nat.find h)) γ'

At the absorbing stage, the transports of the protected components and the strict transforms of the newly absorbed members are protected for the isolated state (the persistence of CP5 for the former, the entry of CP2 for the latter).

theorem Hironaka.Resolution.isolatedTriple_marked_eq_inf_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) (Γs : Finset T.X.left.IdealSheafData) (I₀ : T.X.left.IdealSheafData) (hP : ∀ γ ∈ Γs, ProtectedState T C γ) (hdisj : (↑Γs).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint a.support b.support) (hI₀ : I₀ = (⨅ γ ∈ Γs, γ) ⊓ T.I) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : ((bmoOneRun T hm).take (Nat.find h)).markedTransformSeq I₀ 1 (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length) = (⨅ γ ∈ Finset.image (fun (γ : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq γ (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) Γs ∪ Finset.image (fun (c : T.X.left.IdealSheafData) => ((bmoOneRun T hm).take (Nat.find h)).strictTransformSeq c (Fin.last ((bmoOneRun T hm).take (Nat.find h)).length)) ({c ∈ C | CenterContains (bmoOneRun T hm) c (Nat.find h)}), γ) ⊓ (isolatedTriple T hm C (Nat.find h)).I

The isolation step: at the first absorbing stage Nat.find h of a round whose start satisfies the invariant with the protected set Γs, the invariant is re-established with the enlarged protected set (the transports of Γs and the strict transforms of the newly absorbed members) and the isolated ideal K⁺ = K⁻ : I_abs — CP1 and CP2 for the absorbed members (they miss each other and the Γ̃), and the isolation is the identity near the Γ̃ (stalkIdeal_isolatedTriple_I_eq_of_protectedState).

theorem Hironaka.Resolution.bedAux_pairwise_disjoint_of_protectedStates {k : Type u} [Field k] [CharZero k] (N : ℕ) (T : MarkedTriple k) (hm : T.m = 1) (C Γs : Finset T.X.left.IdealSheafData) : C.card = N → InvCE T.I T.E C → (∀ γ ∈ Γs, ProtectedState T C γ) → ((↑Γs).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint a.support b.support) → (↑(Γs ∪ C)).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint ((bedAux T hm C).strictTransformSeq a (Fin.last (bedAux T hm C).length)).support ((bedAux T hm C).strictTransformSeq b (Fin.last (bedAux T hm C).length)).support

The loop separates: from a state satisfying the invariant with pairwise disjoint protected components, the final strict transforms of the protected components and of the members are pairwise disjoint. Strong induction on the number of members along bedAux: at an absorbing stage the transported protected set is pairwise disjoint and protected for the isolated state, two distinct members not yet absorbed keep distinct strict transforms, and the induction hypothesis separates everything at the end.

theorem Hironaka.Resolution.bedAux_marked_eq_biInf_of_protectedStates {k : Type u} [Field k] [CharZero k] (N : ℕ) (T : MarkedTriple k) (hm : T.m = 1) (C Γs : Finset T.X.left.IdealSheafData) (I₀ : T.X.left.IdealSheafData) : C.card = N → InvCE T.I T.E C → (∀ γ ∈ Γs, ProtectedState T C γ) → ((↑Γs).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint a.support b.support) → I₀ = (⨅ γ ∈ Γs, γ) ⊓ T.I → (bedAux T hm C).markedTransformSeq I₀ 1 (Fin.last (bedAux T hm C).length) = ⨅ γ ∈ Γs ∪ C, (bedAux T hm C).strictTransformSeq γ (Fin.last (bedAux T hm C).length)

The intersection form along the whole loop (CP6, the sheaf form): from a state whose members satisfy InvCE, protected components Γs (pairwise disjoint protected states) and the un-isolated ideal I₀ = (⨅ γ ∈ Γs, γ) ⊓ T.I, the controlled transform of I₀ along the loop is the ideal of the disjoint union of the final strict transforms of the protected components AND of the members — every member is absorbed by the end (exhaustiveness), and the isolated ideal of the last round is ⊤ ([Kol07, Theorem 69 (1)]). Strong induction on C.card through bedAux_of_exists and bedAux_of_not_exists: the intersection form along the round, the isolation step, the protected states of CP5 for the enlarged set.

theorem Hironaka.Resolution.markedTransformSeq_bedAux_last_eq_prod {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) : ((↑C).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint ((bedAux T hm C).strictTransformSeq a (Fin.last (bedAux T hm C).length)).support ((bedAux T hm C).strictTransformSeq b (Fin.last (bedAux T hm C).length)).support) ∧ (bedAux T hm C).markedTransformSeq T.I 1 (Fin.last (bedAux T hm C).length) = ∏ c ∈ C, (bedAux T hm C).strictTransformSeq c (Fin.last (bedAux T hm C).length)

The end identity (the marked_eq and pairwise clauses of the end data): along the whole loop from a state satisfying InvCE, the final strict transforms of the members are pairwise disjoint and the marked transform of the ideal is their PRODUCT — from the intersection form along the loop at Γs = ∅, K_end = ⊤ at the end (CP5), and ⨅ = ∏ for pairwise disjoint strict transforms. The pair that the clauses consume (strictTransformSeq_eq_prod_of_pairwise_disjoint, hasSncWith_prod_of_pairwise_disjoint; [Kol07, 72] for clause (e)).