The skipped round: a round of order reduction that pulls back to empty blow-ups

The second clause of [Kol07, 34.1], that the blow-up sequence of the pull-back along a smooth h : Y → X is the pull-back of the blow-up sequence with the blow-ups of empty centre deleted, for the loops of Steps 1 and 2 of the proof of [Kol07, Theorem 107] rests on the following observation, not in the sources as such: a round of an order-d functor B on X whose pull-back data on Y have max-ord < d pulls back to empty blow-ups only, and the pulled-back end data are the data of Y up to unit boundary members. Every centre of the round lies at points of order exactly d for the current ideal (condition (4) of [Kol07, Definition 66] at the generic points, at every point by upper semicontinuity), whose smooth pull-backs have the same order, and Y has none; once the earlier pulled-back centres are empty, the pulled-back ideal at the next stage is the inverse image of h^* I along an isomorphism, again of order < d. So every pulled-back centre is the unit ideal (center_pullback_eq_top_of_forall_ord_lt, by induction along the round with the one-step transport weakTransform_comap_of_orderAlong_of_equidim), and the four conclusions are those of Hironaka/Resolution/Algebraic/Kol07/TopCenters.lean: the erased pull-back is the empty sequence, its composite is an isomorphism, the weak transform at its end is the inverse image of Y's ideal, and its end boundary is Y's boundary with the unit exceptional members appended (IsTopErasure, the shape of the indifference to empty boundary members). Only the order condition of B enters; commutation of B with smooth morphisms is not assumed. Used in Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothLoop.lean.

theorem Hironaka.Sequence.center_pullback_eq_top_of_forall_ord_lt {k : Type u} [Field k] [CharZero k] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (h : Y ⟶ X) [AlgebraicGeometry.Smooth h] (n' : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n' (CategoryTheory.CategoryStruct.comp h f)] (S : X.BlowUpSequence) {I : X.IdealSheafData} {E : X.DivisorFamily} {d : ℕ} : S.IsOrderSeq f I E d → (∀ (y : ↥Y), (I.comap h).ord y < ↑d) → ∀ (i : Fin (S.pullback h).length), (S.pullback h).center i = ⊤

The core of the skipped-round argument: along a smooth blow-up sequence of order d for (X, I, E), if the pull-back of I along a smooth h : Y ⟶ X has order < d at every point of Y, every centre of the pulled-back sequence is the unit ideal. The first because the points of the centre have order ≥ d for I and their preimages the same order for h^* I; the later ones by induction on the tail, whose starting ideal is the inverse image of h^* I along the trivial blow-up, of order < d again.

theorem Hironaka.BMO.pullback_eraseEmpty_eq_nil_of_maxOrd_lt {k : Type u} [Field k] [CharZero k] {d : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k d Dom) (T T' : AlgebraicGeometry.Triple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOf T h) (hT : Dom T) (hlt : T'.I.maxOrd < ↑d) : ((B.seq T hT).pullback h).eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left ∧ CategoryTheory.IsIso ((B.seq T hT).pullback h).composite ∧ ((B.seq T hT).pullback h).weakTransformSeq T'.I (Fin.last ((B.seq T hT).pullback h).length) = T'.I.comap ((B.seq T hT).pullback h).composite ∧ ∃ (e : T'.E.ι ↪o (((B.seq T hT).pullback h).totalTransformSeq T'.E (Fin.last ((B.seq T hT).pullback h).length)).ι), Sequence.IsTopErasure (T'.E.comap ((B.seq T hT).pullback h).composite) (((B.seq T hT).pullback h).totalTransformSeq T'.E (Fin.last ((B.seq T hT).pullback h).length)) e

A round of an order-d functor on X whose pull-back to Y has max-ord < d pulls back to empty blow-ups only, and the pulled-back end data are the data of Y up to unit boundary members (the second clause of [Kol07, 34.1], for one round): every centre of the round lies at points of order d for the current ideal, whose smooth pull-backs have the same order, and Y has none; so after deleting the empty blow-ups the pulled-back round is the empty sequence, its composite is an isomorphism, the weak transform at its end is the pull-back of Y's ideal, and its end boundary is Y's boundary with the unit exceptional divisors of the empty blow-ups appended (IsTopErasure). Only the order condition of B enters.