Upper semicontinuity of the order function

[Kol07, Definition 47]: "It is easy to see that x ↦ ord_x I is a constructible and upper-semi-continuous function on X." The characteristic-zero route through derivatives ([Kol07, Lemma 74 (3)]; [Wlo05, Lemma 2.6.2], supp(I, μ) = V(D^{μ−1}(I)) is closed): on a scheme smooth of relative dimension n over a field k of characteristic zero,

• {x : ord_x I ≥ m} = V(D^{m−1} I) for m ≥ 1, the cosupport transfer of Hironaka/Scheme/IdealSheaf/Derivative/Cosupport.lean (le_ord_iff_mem_support_derivativeIter) read as an equality of sets (setOf_le_ord_eq_support_derivativeIter);
• {ord ≥ m} is closed for every m ∈ ℕ (m = 0: the whole space; m ≥ 1: a support, closed by Mathlib's isClosed_supportSet), and {ord = ∞} = ⋂_m {ord ≥ m} is closed; it is {x : I_x = 0} by Krull (ord_eq_top_iff, for X locally Noetherian, automatic for a scheme locally of finite type over a field, isLocallyNoetherian_of_field);
• x ↦ ord_x I is upper semicontinuous into ℕ∞ with its order topology, Mathlib's UpperSemicontinuous, that is, every {x : ord_x I ≥ y} is closed (upperSemicontinuous_iff_isClosed_preimage), which is the previous point for y = m and y = ∞.

Used for the constructibility and the finiteness of the order (Hironaka/Scheme/IdealSheaf/Order/Constructible.lean), for its monotonicity along specialization (Hironaka/Scheme/IdealSheaf/Order/Specialization.lean), and directly in Hironaka/Resolution/Algebraic/Hir64/OrderProduct.lean, Hironaka/Resolution/Algebraic/Hir64/Corollary1.lean, Hironaka/Resolution/Algebraic/Hir64/TrivializationLoci.lean, Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivSigma.lean, Hironaka/Resolution/Algebraic/MaximalContact/Existence.lean and on manifolds (Hironaka/Manifold/IdealSheaf/Order.lean).

theorem AlgebraicGeometry.Scheme.Hom.isLocallyNoetherian_of_field {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : IsLocallyNoetherian X

A scheme locally of finite type over a field is locally Noetherian: on every affine open the ring of sections is a finitely generated k-algebra, hence Noetherian.

theorem AlgebraicGeometry.Scheme.IdealSheafData.setOf_ord_eq_top_eq_iInter {X : Scheme} (I : X.IdealSheafData) : {x : ↥X | I.ord x = ⊤} = ⋂ (m : ℕ), {x : ↥X | ↑m ≤ I.ord x}

The infinite level set as an intersection: {ord = ∞} = ⋂_m {ord ≥ m}.

theorem AlgebraicGeometry.Scheme.IdealSheafData.setOf_ord_eq_top_eq_setOf_stalkIdeal_eq_bot {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (I : X.IdealSheafData) : {x : ↥X | I.ord x = ⊤} = {x : ↥X | I.stalkIdeal x = ⊥}

{ord = ∞} = {x : I_x = 0} on a scheme locally of finite type over a field (Krull's intersection theorem).

theorem AlgebraicGeometry.Scheme.IdealSheafData.setOf_le_ord_eq_support_derivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hm : 1 ≤ m) : {x : ↥X | ↑m ≤ I.ord x} = ↑(derivativeIter f (m - 1) I).support

[Kol07, Lemma 74 (3)]; [Wlo05, Lemma 2.6.2]: {x : ord_x I ≥ m} = V(D^{m−1} I) for m ≥ 1, the cosupport transfer as an equality of sets.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_setOf_le_ord {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m : ℕ) : IsClosed {x : ↥X | ↑m ≤ I.ord x}

{x : ord_x I ≥ m} is closed for every m ∈ ℕ (for m = 0 it is X; for m ≥ 1 it is the support V(D^{m−1} I)).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_setOf_ord_eq_top {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) : IsClosed {x : ↥X | I.ord x = ⊤}

{x : ord_x I = ∞} is closed.

theorem AlgebraicGeometry.Scheme.IdealSheafData.upperSemicontinuous_ord {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) : UpperSemicontinuous fun (x : ↥X) => I.ord x

[Kol07, Definition 47]: x ↦ ord_x I is upper semicontinuous into ℕ∞ with its order topology — every {x : ord_x I ≥ y} is closed.