The round parameters of Steps 1 and 2 under a change of fields

[Kol07, 34.2]: the change of fields σ : k → L replaces (X, I, m, E) by (X_L, I_L, m, E_L) along the projection p : X_L → X, which is flat and surjective on points. The round parameter of Step 1, d = max-ord N(I), and that of Step 2, s = max-ord_{cosupp(I, m)} N(I), are preserved: the split pulls back (nonmonomialPart_baseChange), the maximal order is preserved by a change of fields (maxOrd_comap_of_isPullback_specMap, through the derivative), and the order at every point of X_L is the order at its image (ord_comap_of_isPullback_specMap: the support of a marked ideal is the support of an iterated derivative, [Wlo05, Lemma 2.6.2], and the derivative commutes with the base-change square). These are the change-of-fields forms of Hironaka/Resolution/Algebraic/MarkedOrderReduction/Parameters.lean, used in Hironaka/Resolution/Algebraic/MarkedOrderReduction/BaseChangeLoop.lean. Not in the sources as such.

theorem Hironaka.BMO.ord_comap_of_isBaseChangeOf {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] {T : AlgebraicGeometry.Triple k} {T' : AlgebraicGeometry.Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hbc : T'.IsBaseChangeOf T σ p) (I : T.X.left.IdealSheafData) (y : ↥T'.X.left) : (I.comap p).ord y = I.ord (p y)

The order at a point of the base-changed triple is the order at its image ([Kol07, 34.2]).

theorem Hironaka.BMO.maxOrd_comap_of_isBaseChangeOf {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] {T : AlgebraicGeometry.Triple k} {T' : AlgebraicGeometry.Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hbc : T'.IsBaseChangeOf T σ p) (J : T.X.left.IdealSheafData) : (J.comap p).maxOrd = J.maxOrd

The maximal order is preserved by a change of fields ([Kol07, 34.2]; maxOrd_comap_of_isPullback_specMap at the triple).

theorem Hironaka.BMO.maxOrdAlong_comap_preimage_of_isBaseChangeOf {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] {T : AlgebraicGeometry.Triple k} {T' : AlgebraicGeometry.Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hbc : T'.IsBaseChangeOf T σ p) (J : T.X.left.IdealSheafData) (Z : Set ↥T.X.left) : (J.comap p).maxOrdAlong (⇑p ⁻¹' Z) = J.maxOrdAlong Z

The maximal order of the base-changed ideal along the preimage of a set is the maximal order along the set: the order is preserved pointwise and the projection is surjective.

theorem Hironaka.BMO.roundOrder_of_isBaseChangeOf {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (T : MarkedTriple k) (T' : MarkedTriple L) {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hbc : T'.IsBaseChangeOf T σ p) : roundOrder T' = roundOrder T

The round parameter of Step 1 is preserved by change of fields ([Kol07, 34.2]): nonmonomialPart_baseChange, and the base change preserves the maximal order.

theorem Hironaka.BMO.sepOrder_of_isBaseChangeOf {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (T : MarkedTriple k) (T' : MarkedTriple L) {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (hbc : T'.IsBaseChangeOf T σ p) : sepOrder T' = sepOrder T

The separation parameter of Step 2 is preserved by change of fields ([Kol07, 34.2]).