Two marked ideals with the same nonmonomial part keep it along a common sequence

In Step 2 of the proof of [Kol07, Theorem 107] ([Kol07, 111, Step 2]) a round of order reduction for N(I)^m + I^s is at once a smooth blow-up sequence of order ≥ s for (N(I), s) and of order ≥ m for (I, m); after it, "we stop when cosupp(I_r, m) ∩ cosupp(N(I_r), s) = ∅", which compares the nonmonomial part N(I_r) of the new marked ideal with the marked transform N_r := Π^{-1}_*(N(I), s) of the old one. The comparison is the invariant proved here, not in the sources as such: for two marked ideals (I, m) and (J, s) on the same triple with N(I) = N(J), along a smooth blow-up sequence of order ≥ m for the first and ≥ s for the second, the nonmonomial parts of the two induced marked ideals agree at the end. One blow-up is the identity N(π^{-1}_*(I, m)) = N(π^* N(I)) of Hironaka/Resolution/Algebraic/MarkedOrderReduction/Transform.lean (nonmonomialPart_markedTransform), applied to both marked triples: N(I_{i+1}) = N(π^* N(I_i)) = N(π^* N(J_i)) = N(J_{i+1}). The variant with the second sequence unmarked at the exact order, used for the rounds of Step 1, is nonmonomialPart_markedTransformSeq_last_eq in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step1NonmonomialPart.lean.

• nonmonomialPart_markedTransformSeq_eq_of_isOrderGeSeq: the invariant at the end of the sequence, through nonmonomialPart_markedTransformSeq_eq_of_isOrderGeSeq_aux by induction on the length (the marked triples advance to blowUpTriple, so the induction is on the length, not structural on a sequence over a fixed scheme).

theorem Hironaka.BMO.nonmonomialPart_markedTransformSeq_eq_of_isOrderGeSeq_aux {k : Type u} [Field k] [CharZero k] (l : ℕ) (T : MarkedTriple k) (S : T.X.left.BlowUpSequence) : S.length = l → ∀ {J : T.X.left.IdealSheafData}, J.IsNonzeroEverywhere → ∀ {s : ℕ}, S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) J s T.E → S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E → nonmonomialPart T.I T.E = nonmonomialPart J T.E → nonmonomialPart (S.markedTransformSeq T.I T.m (Fin.last S.length)) (S.totalTransformSeq T.E (Fin.last S.length)) = nonmonomialPart (S.markedTransformSeq J s (Fin.last S.length)) (S.totalTransformSeq T.E (Fin.last S.length))

The recursion behind nonmonomialPart_markedTransformSeq_eq_of_isOrderGeSeq, by induction on the length of the sequence.

theorem Hironaka.BMO.nonmonomialPart_markedTransformSeq_eq_of_isOrderGeSeq {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (S : T.X.left.BlowUpSequence) {J : T.X.left.IdealSheafData} (hJ : J.IsNonzeroEverywhere) {s : ℕ} (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) J s T.E) (hge : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) (hN : nonmonomialPart T.I T.E = nonmonomialPart J T.E) : nonmonomialPart (S.markedTransformSeq T.I T.m (Fin.last S.length)) (S.totalTransformSeq T.E (Fin.last S.length)) = nonmonomialPart (S.markedTransformSeq J s (Fin.last S.length)) (S.totalTransformSeq T.E (Fin.last S.length))

For two marked ideals (I, m) and (J, s) on the same triple with N(I) = N(J), along a smooth blow-up sequence of order ≥ m for (I, m) and of order ≥ s for (J, s), the nonmonomial parts of the induced marked ideals agree at the end, with respect to the induced boundary: nonmonomialPart_markedTransform applied to both marked triples at every stage (the identity "N((Π_1)^{-1}_*(I, m)) = (Π_1)^{-1}_* N(I)" of [Kol07, 111, Step 1], read modulo N). Step 2 of the proof of Theorem 107 uses it at J = N(I) and s the separation order: N(I_r) = N(Π^{-1}_*(N(I), s)). Not in the sources as such.