The round parameters under smooth surjective pull-back

The first clause of [Kol07, 34.1] ("B commutes with every smooth surjection h") for the loop variables of Steps 1 and 2 of the proof of [Kol07, Theorem 107]: the round order d = max-ord N(I) (roundOrder, Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step1NonmonomialPart.lean) and the separation order s = max-ord_{cosupp(I, m)} N(I) (sepOrder, Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step2Separation.lean) of a marked triple are unchanged by a smooth surjective pull-back. The split pulls back (N(h^* I) = h^* N(I), nonmonomialPart_comap), the order of a smooth pull-back at a point is the order at the image (ord_comap_of_smooth), and a surjection preserves maxima (maxOrd_comap_of_surjective, maxOrdAlong_comap_preimage_of_surjective). Consequently the loops of Steps 1 and 2 on Y run in step with those on X (Hironaka/Resolution/Algebraic/MarkedOrderReduction/LoopFunctorial.lean). Not in the sources as such.

theorem Hironaka.BMO.maxOrd_comap_of_surjective {X Y : AlgebraicGeometry.Scheme} (J : X.IdealSheafData) (h : Y ⟶ X) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) : (J.comap h).maxOrd = J.maxOrd

The maximal order of a smooth surjective pull-back is the maximal order (maxOrd_comap_le_of_smooth and maxOrd_le_maxOrd_comap_of_surjective).

theorem Hironaka.BMO.maxOrdAlong_comap_preimage_of_surjective {X Y : AlgebraicGeometry.Scheme} (J : X.IdealSheafData) (h : Y ⟶ X) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (Z : Set ↥X) : (J.comap h).maxOrdAlong (⇑h ⁻¹' Z) = J.maxOrdAlong Z

The maximal order of a smooth surjective pull-back along the preimage of a set is the maximal order along the set.

theorem Hironaka.BMO.roundOrder_of_isPullbackOf {k : Type u} [Field k] [CharZero k] (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hp : T'.IsPullbackOf T h) : roundOrder T' = roundOrder T

The round parameter d = max-ord N(I) of Step 1 is preserved by smooth surjective pull-back: the split pulls back (nonmonomialPart_comap) and a surjection preserves the maximal order.

theorem Hironaka.BMO.sepOrder_of_isPullbackOf {k : Type u} [Field k] [CharZero k] (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hp : T'.IsPullbackOf T h) : sepOrder T' = sepOrder T

The separation parameter s of Step 2 is preserved by smooth surjective pull-back: the cosupport and the nonmonomial part pull back.