The monomial split, IV: smooth pull-back and change of fields

M(h^* I) = h^* M(I) and N(h^* I) = h^* N(I) for a smooth h, and likewise along a change of fields: the two functoriality inputs of [Kol07, 34.1] and [Kol07, 34.2] for the marked order reduction, whose construction is built on the split. Both are the case of a flat morphism p : Y → X between the schemes of two triples carrying the pulled-back data (p^* I, p^{-1} E): the irreducible components of p^{-1} E^i are the components of the p^{-1} D (a generic point of p^{-1} E^i lies over a generic point of E^i, mem_genericPoints_support_of_flat), the order of p^* I at such a generic point is the order of I at its image (ord_comap_of_flat_of_stalkIdeal_eq, the stalks of the members being the maximal ideals at the generic points), and the stalk of p^* 𝓘_D at a point y is the image of the stalk of 𝓘_D at p y; so the stalks of M(p^* I) and of p^* M(I) agree at every y. The nonmonomial part follows by the uniqueness of the split on Y.

• monomialPart_comap_of_flat, nonmonomialPart_comap_of_flat: for a flat p into a triple's scheme from a scheme smooth over a field, with the pulled-back family having normal crossings. The forms on triples, for a smooth morphism and for a change of fields, are in Hironaka/Resolution/Algebraic/MarkedOrderReduction/SplitTriple.lean.

theorem Hironaka.BMO.monomialPart_comap_of_flat {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {Y : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥Y] (p : Y ⟶ T.X.left) [AlgebraicGeometry.Flat p] (hsnc' : (T.E.comap p).IsSnc) : monomialPart (T.I.comap p) (T.E.comap p) = (monomialPart T.I T.E).comap p

M(p^* I) = p^* M(I): the monomial part of the pulled-back data along a flat p is the pull-back of the monomial part.

theorem Hironaka.BMO.nonmonomialPart_comap_of_flat {k L : Type u} [Field k] [Field L] (T : AlgebraicGeometry.Triple k) {Y : AlgebraicGeometry.Scheme} (g : Y ⟶ AlgebraicGeometry.Spec ↧L) [AlgebraicGeometry.Smooth g] [TopologicalSpace.NoetherianSpace ↥Y] (p : Y ⟶ T.X.left) [AlgebraicGeometry.Flat p] (hsnc' : (T.E.comap p).IsSnc) [CharZero k] [CharZero L] : nonmonomialPart (T.I.comap p) (T.E.comap p) = (nonmonomialPart T.I T.E).comap p

N(p^* I) = p^* N(I): the nonmonomial part of the pulled-back data along a flat p is the pull-back of the nonmonomial part. p^* I = p^* M(I) · p^* N(I) with p^* M(I) the monomial part of p^* I and p^* N(I) of order 0 at every component's generic point, so it is the nonmonomial part by uniqueness.