Włodarczyk's Claim along Step 1: the rounds of order ≥ 2 and the end of Step 1

Włodarczyk's proof of his Claim in the proof of [Wlo05, Theorem 4.7.1] passes through the purely nonmonomial stage ("At this stage I = N(I) is purely nonmonomial") before restricting to a hypersurface of maximal contact. In Kollár's order (Step 1 of the proof of [Kol07, Theorem 107], item 111) the run of BMO_{n,1} on (X, I, 1, E) is step1 ++ step2 ++ step3, and Step 1 is the sequence of rounds BO_{n,d}(X, N(I), E) for d = max-ord N(I) decreasing to below 1 (Hironaka.Resolution.Algebraic.MarkedOrderReduction.Step1NonmonomialPart). For the member c = I_{closure η} of Włodarczyk's Claim, with η ∉ E and I = c at η:

• a round of order d ≥ 2 never blows up a centre containing the strict transform c̃: the nonmonomial part has order 1 at the generic point η̃ of c̃ (GenericLift.ord_eq_one), while the centres of the round carry order d ≥ 2 for the weak transform of N(I), which contains the marked transform (markedTransformSeq_le_weakTransformSeq_of_le); upper semicontinuity of the order (not_centerContains_of_leOrdAlong_two) excludes η̃ from every centre;
• the round of order 1 is BO_{n,1}(X, N(I), E), where the conclusion of Włodarczyk's Claim for BO_{n,1} (ClaimBOFor) concerns the purely nonmonomial triple (X, N(I), E), which satisfies the hypotheses of the Claim at η;
• after Step 1 the nonmonomial part has maximal order < 1 (maxOrd_nonmonomialPart_step1_lt), so no lift of η survives: the first containing centre lies in Step 1.

ClaimBOFor is the conclusion ClaimFor (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimAt) for BO_{n,1}; since ClaimKC is false for the transcribed order (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses), it is not available at every stage of the tower, and the module is used only through its lemmas on the rounds of order ≥ 2 and on the end of Step 1, which Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step1 uses for the induction on the loop variable d, mirroring the recursion of step1, with the chain-relative conclusion of CP1.

The nonmonomial part off the boundary

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_of_forall_notMem {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] [TopologicalSpace.NoetherianSpace ↥X] (I : X.IdealSheafData) (E : X.DivisorFamily) {x : ↥X} (hx : ∀ (i : E.ι), x ∉ (E.component i).support) : (BMO.nonmonomialPart I E).stalkIdeal x = I.stalkIdeal x

Off every member of the boundary the nonmonomial part is the ideal itself, stalkwise.

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

The conclusion of Włodarczyk's Claim for the run of BO_{n,1} of a family bo of order-reduction data over the field k, stated for every triple of BOClass n 1 (the hypothesis of the reduction from BMO_{n,1}).

Equations

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

The hypotheses of Włodarczyk's Claim for the purely nonmonomial triple

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_triple_eq {k : Type u} [Field k] (T : MarkedTriple k) {η : ↥T.X.left} (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) : (BMO.nonmonomialPart T.I T.E).stalkIdeal η = T.I.stalkIdeal η

At η ∉ E the nonmonomial part agrees with I.

theorem Hironaka.Resolution.mem_genericPoints_nonmonomialPart_support {k : Type u} [Field k] (T : MarkedTriple k) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) : η ∈ (BMO.nonmonomialPart T.I T.E).support.genericPoints

η is a generic point of the support of N(I): it lies there (N(I) = I at η) and the support of N(I) lies in that of I.

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_triple_eq_closure {k : Type u} [Field k] (T : MarkedTriple k) {η : ↥T.X.left} (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : (BMO.nonmonomialPart T.I T.E).stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η

N(I) agrees with c at η.

theorem Hironaka.Resolution.stalkIdeal_nonmonomialPart_triple_ne_bot {k : Type u} [Field k] (T : MarkedTriple k) {η : ↥T.X.left} (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) : (BMO.nonmonomialPart T.I T.E).stalkIdeal η ≠ ⊥

N(I) is nonzero at η.

A round of order ≥ 2 never contains the strict transform

theorem Hironaka.Resolution.not_centerContains_step1Round_of_two_le {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hd : m ≤ BMO.roundOrder T) (h2 : 2 ≤ BMO.roundOrder 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 η) (l : ℕ) : ¬CenterContains (BMO.step1Round bo T hT hd) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) l

No centre of a round BO_{n,d}(X, N(I), E) with d ≥ 2 contains the strict transform of c = I_{closure η} (Step 1 of the proof of [Kol07, Theorem 107], the rounds of order d ≥ 2): at the generic point of the strict transform at the first such stage the weak transform of N(I) has order ≤ 1, while the centre carries order d ≥ 2.

After Step 1 no lift survives

theorem Hironaka.Resolution.not_genericLift_step1_last {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n 1 T) {η : ↥T.X.left} (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (η' : ↥((↑(BMO.step1 bo T hT)).stage (Fin.last (↑(BMO.step1 bo T hT)).length))) (hlift : GenericLift (↑(BMO.step1 bo T hT)) T.I T.E 1 η (Fin.last (↑(BMO.step1 bo T hT)).length) η') : False

The lift of η cannot reach the end of Step 1 (Step 1 of the proof of [Kol07, Theorem 107] ends with max-ord N(I) < m): there the nonmonomial part has maximal order < 1, while at a lift its stalk is the maximal ideal. So the first centre containing c̃ lies in Step 1.