The cosupport of the maximal contact ideal is the locus of order at least m

Kollár's maximal contact ideal is the (m−1)-st derivative MC(I) := D^{m−1}(I) of an ideal sheaf I of maximal order m; it has order 1 at the points where I has order m and order 0 where I has smaller order, so that "cosupp MC(I) = cosupp(I, m)" [Kol07, Definition 79]. On an analytic manifold, for m ≥ 1, the cosupport of D^{m−1}(J) is the locus {a | m ≤ ν_a(J)} (cosupport_iteratedDeriv): the cosupport of a locally finitely generated ideal sheaf, hence closed. The proof is [Kol07, Lemma 74 (3)] at the stalk — m ≤ ord I ↔ m − r ≤ ord Dʳ(I) for r < m, in the Hironaka library's regular coordinates of the stalk (le_ord_iff_le_ord_Dpow), which the analytic stalk carries (exists_regularCoords_stalk, once it is a regular local ring of dimension n) — through stalkIdeal_iteratedDeriv_eq_Dpow. Consequently {a | ν_a(J) ≤ k} is open (isOpen_setOf_ord_le), the upper semicontinuity of the order in the form the order-reduction algorithm uses. Bierstone–Milman's locally Noetherian hypothesis on their category of spaces [BM97, (3.8)(3); Definitions and remarks 3.9] is not needed for this: the closedness of the locus comes from the local finite generation of the derivative ideal sheaves.

theorem Manifold.IdealSheaf.support_iteratedDeriv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : 1 ≤ m) : (J.iteratedDeriv (m - 1)).support = {a : ↑↧M | ↑m ≤ J.ord a}

Kollár's "cosupp MC(I) = cosupp(I, m)" [Kol07, Definition 79], from [Kol07, Lemma 74 (3)]: for m ≥ 1, the cosupport of D^{m−1}(J) is the locus where the order of J is at least m.

The order is upper semicontinuous: {ord ≤ k} is open

theorem Manifold.IdealSheaf.isOpen_setOf_ord_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (k : ℕ) : IsOpen {y : M.carrier | ord I y ≤ ↑k}

{ord 𝓘 ≤ k} is open: its complement {ord 𝓘 ≥ k + 1} is the cosupport of the derivative ideal sheaf D^k 𝓘, a closed set.