The final maximal order along a concatenation

weakTransformSeq_concat_last (Hironaka/Scheme/BlowUpSequence/ConcatApi.lean) identifies the final weak transform along S.concat T with the final weak transform along T of the final weak transform along S, up to the identification eqToHom (last_concat S T) of the last stages. The maximal order does not see that identification (maxOrd_comap_eqToHom), so the two maximal orders agree (maxOrd_weakTransformSeq_concat_last). This is what the maximal contact case of the proof of Theorem 103 needs to read the conclusion max-ord I_r < m for the boundary-clearing sequence followed by the restriction to the hypersurface from the latter alone [Kol07, 104, Step 2.2].

theorem AlgebraicGeometry.maxOrd_comap_eqToHom {X Y : Scheme} (h : X = Y) (J : Y.IdealSheafData) : (J.comap (CategoryTheory.eqToHom h)).maxOrd = J.maxOrd

The maximal order of an ideal sheaf is unchanged by the inverse image along the identification of two equal schemes.

theorem AlgebraicGeometry.maxOrd_weakTransformSeq_concat_last {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (J : X.IdealSheafData) : ((S.concat T).weakTransformSeq J (Fin.last (S.concat T).length)).maxOrd = (T.weakTransformSeq (S.weakTransformSeq J (Fin.last S.length)) (Fin.last T.length)).maxOrd

The maximal order of the final weak transform along a concatenation is that along the second part of the weak transform along the first (the eqToHom of last_concat does not change max-ord).