The maximal order is antitone in the ideal sheaf

[Kol07, Definition 47]: ord_x I ≥ r iff I_x ⊆ 𝔪_x^r, and max-ord I := max{ord_x I : x ∈ X}. A larger ideal sheaf has a smaller order at every point (ord_anti, Hironaka/Scheme/IdealSheaf/Order/Basic.lean), hence a smaller maximal order:

• maxOrd_anti: I ≤ J → max-ord J ≤ max-ord I;
• maxOrdAlong_anti: the same along a subset Z.

Used in the first step of the proof of [Kol07, Theorem 107] ([Kol07, 111]) in the form max-ord N(J) ≤ max-ord J for the nonmonomial part N(J) ⊇ J (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step1NonmonomialPart.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/Clause3.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step2Separation.lean).

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrdAlong_anti {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (Z : Set ↥X) : J.maxOrdAlong Z ≤ I.maxOrdAlong Z

The maximal order along a subset is antitone in the ideal sheaf — pointwise ord_anti under the supremum.

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrd_anti {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) : J.maxOrd ≤ I.maxOrd

The maximal order is antitone in the ideal sheaf, I ≤ J → max-ord J ≤ max-ord I; in its use, max-ord N(J) ≤ max-ord J since J ⊆ N(J).