The state of the loop after an isolation, in index form

In the isolation passage of the proof of [Wlo05, Theorem 4.7.1], after the isolation the loop restarts on (X_n, I_n : I_Γ, E_n) with the remaining components, the absorbed ones "ignored". This module shows that the state of the loop (EmbeddedStateData, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedState) is restored at the absorbing stage, read in the index form of the stages of the run: the strict transforms of the remaining members satisfy the invariant (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedRemaining); the absorbed strict transforms join the protected components — with simple normal crossings, contained in no member (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNotContained), pairwise disjoint, disjoint from the remaining members, and with the nonmonomial part of the isolated ideal trivial along them (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedIsolatedIdeal); the previously protected components are carried by the protected transport along the run (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedProtected), their disjointness by the preimage of supports, and the triviality of the nonmonomial part along them by the monotonicity of the nonmonomial support along the run (the hypothesis CentersInNonmonomialSupportOrStratum) and at the isolation (nonmonomialPart_le_nonmonomialPart_isolatedMarkedIdeal).

The theorem embeddedStateData_isolated assumes ClaimKC, StratumBlowUp and CentersInNonmonomialSupportOrStratum (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses; the first is false, the other two unproved) and is a CONDITIONAL lemma, used only by the conditional loop (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedStep); the proof of the theorem uses CP5 instead (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5).

noncomputable def Hironaka.Resolution.remainingIdx {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) : Finset ((bmoOneRun T hm).stage (absorbIndex T hm C h).castSucc).IdealSheafData

The remaining members at the absorbing stage, in index form: the strict transforms of the members not absorbed there (remainingComponents of Hironaka.Resolution.Algebraic.Wlo05.Embedded, read at the stage of the run).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hironaka.Resolution.protectedIdx {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (h : ∃ (n : ℕ), HasAbsorptionAt T hm C n) (Γ : Finset T.X.left.IdealSheafData) : Finset ((bmoOneRun T hm).stage (absorbIndex T hm C h).castSucc).IdealSheafData

The protected components at the absorbing stage, in index form: the strict transforms of the previously protected components and of the members absorbed there.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Resolution.embeddedStateData_isolated {k : Type u} [Field k] [CharZero k] {T : MarkedTriple k} {hm : T.m = 1} {C : Finset T.X.left.IdealSheafData} {h : ∃ (n : ℕ), HasAbsorptionAt T hm C n} (hKC : ClaimKC k) (hG : StratumBlowUp k) (hL : CentersInNonmonomialSupportOrStratum k) (Γ : Finset T.X.left.IdealSheafData) (hs : EmbeddedStateData T.I T.E C Γ) : EmbeddedStateData (isolatedMarkedIdeal T hm C h) ((bmoOneRun T hm).totalTransformSeq T.E (absorbIndex T hm C h).castSucc) (remainingIdx T hm C h) (protectedIdx T hm C h Γ)

The state of the loop is restored at the isolation, in index form (the isolation passage of the proof of [Wlo05, Theorem 4.7.1]); conditional on ClaimKC, StratumBlowUp and CentersInNonmonomialSupportOrStratum.