The stage predicates of CP1

The tower induction for the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) runs on two predicates indexed by the stage n of the tower of order reductions (tower stage0 n; [Kol07, 70]), the analogues for CP1 of ClaimBOAt and ClaimBMOAt (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimAt): CP1 along the run of the stage-n order reduction BO_{n,1} on every triple of BOClass n 1, and along the run of the stage-n marked order reduction BMO_{n,1} on every marked triple of BMOClass n 1, for a generic point η of V(I) off the boundary at which I is the component's ideal (the three hypotheses of cp1For_concat, kept verbatim). The run bmoOneRun of the loop is the instance n = T.dim (dimFreeBMO_seq). The predicates are proved along the tower in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step1, EmbeddedCP1Step2 and EmbeddedCP1Tower.

def Hironaka.Resolution.CP1BOAt (k : Type u) [Field k] [CharZero k] (n : ℕ) : Prop

The stage predicate of CP1 for BO_{n,1}: CP1 holds along the run of the stage-n order reduction on every triple of BOClass n 1, for a generic point η of V(I) off the boundary at which I is the component's ideal — the analogue for CP1 of ClaimBOAt.

Equations

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

def Hironaka.Resolution.CP1BMOAt (k : Type u) [Field k] [CharZero k] (n : ℕ) : Prop

The stage predicate of CP1 for BMO_{n,1}: CP1 along the run of the stage-n marked order reduction on every marked triple of BMOClass n 1 — the analogue for CP1 of ClaimBMOAt.

Equations

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