CP1 through Step 1

Step 1 of the proof of [Kol07, Theorem 107] (item 111) runs BMO_{n,1} on (X, I, 1, E) as rounds of BO_{n,d} on the nonmonomial part N(I) for d = max-ord N(I) descending to 1, followed by Steps 2 and 3. Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimStep1 proved, for the conclusion of Włodarczyk's Claim, that the first stage whose centre contains the strict transform of a component lies in the round of order 1 (not_centerContains_step1Round_of_two_le) and that no lift survives Step 1 (not_genericLift_step1_last). This module runs the same induction for the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative; CP1For in place of ClaimFor). The one new step: at the absorbing stage the chain form of the marked transform of N(I), given by CP1 for BO_{n,1} on the nonmonomial triple, gives the chain form of the marked transform of I = N(I) · M(I) by chainRelativeAt_markedTransformSeq_mul_monomial (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainMonomial; the monomial part is E.monomial (fun η => (I.ord η).toNat), monomialPart_eq_monomial). The tower induction is that of [Kol07, 70]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Tower.

def Hironaka.Resolution.CP1BOFor (k : Type u) [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) : Prop

CP1 for the run of BO_{n,1} of a family bo of order-reduction data over k, stated for every triple of BOClass n 1 (the hypothesis of the reduction from BMO_{n,1}; ClaimBOFor with CP1For in place of ClaimFor).

Equations

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

theorem Hironaka.Resolution.cp1For_step1Round_of_roundOrder_eq_one {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) (hbo : CP1BOFor k bo) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n 1 T) (hd : 1 ≤ BMO.roundOrder T) (h1 : BMO.roundOrder T = 1) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For (BMO.step1Round bo T hT hd) T.I T.E η

CP1 for the round of order 1, BO_{n,1}(X, N(I), E), from CP1 for BO_{n,1} on the triple (X, N(I), E) (Step 1 of the proof of [Kol07, Theorem 107] at d = 1): the chain form of the marked transform of N(I) at the absorbing stage gives that of I = N(I) · M(I) by chainRelativeAt_markedTransformSeq_mul_monomial.

theorem Hironaka.Resolution.cp1For_step1_aux {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) (hbo : CP1BOFor k bo) (l : ℕ) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n 1 T) : BMO.roundOrder T ≤ l → ∀ η ∈ T.I.support.genericPoints, (∀ (i : T.E.ι), η ∉ (T.E.component i).support) → T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η → CP1For (↑(BMO.step1 bo T hT)) T.I T.E η

CP1 for Step 1 on a marked triple of mark 1 (Step 1 of the proof of [Kol07, Theorem 107], the loop on d = max-ord N(I)), by induction on a bound for the loop variable: a round of order ≥ 2 contains no centre with c̃ (not_centerContains_step1Round_of_two_le), the round of order 1 has CP1 from BO_{n,1} (cp1For_step1Round_of_roundOrder_eq_one), and the rest of Step 1 has it by induction on the induced marked triple with the lifted member (cp1For_concat, GenericLift).

theorem Hironaka.Resolution.cp1For_bmoSeq {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) (hbo : CP1BOFor k bo) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n 1 T) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For (BMO.bmoSeq bo T hT) T.I T.E η

CP1 for the run of BMO_{n,1} from CP1 for BO_{n,1} (the proof of [Kol07, Theorem 107], item 111): the run is step1 ++ (step2 ++ step3), Step 1 has CP1 by the induction on the loop variable, and no lift of η reaches the end of Step 1 (not_genericLift_step1_last).

theorem Hironaka.Resolution.cp1BMOAt_succ_of_cp1BOAt {k : Type u} [Field k] [CharZero k] (n : ℕ) (hbo : CP1BOAt k (n + 1)) : CP1BMOAt k (n + 1)

The Step 1 reduction along the tower ([Kol07, 70, (70.2)]: (68) in dimension n gives (69) in dimension n): CP1 for BMO_{n+1,1} from CP1 for BO_{n+1,1}.