Monotonicity of the order along specialization

[Hau03, Appendix A]: ord_Z = min_{a ∈ Z} ord_a I, "where it suffices to take the minimum over the closed points a of Z", and the order "does not increase under localization" (Hauser refers to Zariski and Nagata for this). Here: if x ∈ closure {η} then ord_η I ≤ ord_x I, which is the content of the upper semicontinuity of Hironaka/Scheme/IdealSheaf/Order/Semicontinuity.lean; in characteristic zero it replaces the Zariski–Nagata argument.

• The general form: for an ideal sheaf I whose order function is upper semicontinuous, a closed set {x : ord_x I ≥ y} containing η contains every specialization of η (ord_le_ord_of_specializes_of_upperSemicontinuous); hence the generic point of an irreducible closed Z has the smallest order on Z (ordAlong_le_ord_of_upperSemicontinuous, ordAlong_eq_iInf_of_upperSemicontinuous), the minimum may be taken over the closed points of Z when the closed points are dense in every locally closed subset (a Jacobson space, ordAlong_eq_iInf_closedPoints_of_upperSemicontinuous), and Kollár's convention ord_Z I ≥ m for a reducible closed Z (Hironaka/Scheme/IdealSheaf/Order/Along.lean) is the pointwise bound on Z (leOrdAlong_iff_forall_mem_of_upperSemicontinuous), since every point of a closed set is a specialization of one of its generic points (Closeds.exists_mem_genericPoints_specializes, by Zorn's lemma inside Z as in Mathlib's exists_preirreducible).
• The same for f : X ⟶ Spec k smooth of relative dimension n over a field k of characteristic zero (upperSemicontinuous_ord; the closed points are dense in every locally closed subset by Mathlib's LocallyOfFiniteType.jacobsonSpace).

Used throughout for the orders at the generic points of centres and along specialization (Hironaka/Scheme/BlowUpSequence/OrderAlongCenter.lean, Hironaka/Scheme/BlowUpSequence/CentersCosupport.lean, Hironaka/Scheme/Snc/DictionaryOrder.lean, Hironaka/Resolution/Algebraic/Balanced/Order.lean, Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/SkippedRound.lean, Hironaka/Resolution/Algebraic/Wlo05/EmbeddedClaimTools.lean, Hironaka/Resolution/Algebraic/Tuning/Corollary101.lean, among others).

theorem TopologicalSpace.Closeds.exists_mem_genericPoints_specializes {X : Type u_1} [TopologicalSpace X] [T0Space X] [QuasiSober X] (Z : Closeds X) {z : X} (hz : z ∈ Z) : ∃ η ∈ Z.genericPoints, η ⤳ z

The topological input for a reducible closed Z (Kollár's convention, [Kol07, Definition 47]): in a sober T₀ space every point z of a closed set Z is a specialization of a generic point of Z — a maximal irreducible closed subset of Z through z exists (Zorn, as in Mathlib's exists_preirreducible), and its generic point is a generic point of Z (Closeds.mem_genericPoints_iff).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_le_ord_of_specializes_of_upperSemicontinuous {X : Scheme} (I : X.IdealSheafData) (hI : UpperSemicontinuous fun (x : ↥X) => I.ord x) {η x : ↥X} (h : η ⤳ x) : I.ord η ≤ I.ord x

General form of "does not increase under localization" ([Hau03, Appendix A]): when x ↦ ord_x I is upper semicontinuous, ord_η I ≤ ord_x I for η ⤳ x — the closed set {ord ≥ ord_η I} contains η, hence x.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlong_le_ord_of_upperSemicontinuous {X : Scheme} (I : X.IdealSheafData) (hI : UpperSemicontinuous fun (x : ↥X) => I.ord x) (Z : TopologicalSpace.IrreducibleCloseds ↥X) {z : ↥X} (hz : z ∈ Z) : I.ordAlong Z ≤ I.ord z

General form: the generic point of an irreducible closed Z has the smallest order on Z.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlong_eq_iInf_of_upperSemicontinuous {X : Scheme} (I : X.IdealSheafData) (hI : UpperSemicontinuous fun (x : ↥X) => I.ord x) (Z : TopologicalSpace.IrreducibleCloseds ↥X) : I.ordAlong Z = ⨅ z ∈ ↑Z, I.ord z

[Hau03, Appendix A], general form: ord_Z I = min_{z ∈ Z} ord_z I for an irreducible closed Z (attained at the generic point).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlong_eq_iInf_closedPoints_of_upperSemicontinuous {X : Scheme} (I : X.IdealSheafData) (hI : UpperSemicontinuous fun (x : ↥X) => I.ord x) [JacobsonSpace ↥X] (Z : TopologicalSpace.IrreducibleCloseds ↥X) : I.ordAlong Z = ⨅ z ∈ ↑Z ∩ closedPoints ↥X, I.ord z

[Hau03, Appendix A], "it suffices to take the minimum over the closed points", general form: in a Jacobson space (closed points dense in every locally closed subset), ord_Z I is the minimum of ord_a I over the closed points a ∈ Z: when ord_Z I = m < ∞, the locally closed set Z ∖ {ord ≥ m + 1} contains the generic point, hence a closed point a, and ord_a I ≤ m.

theorem AlgebraicGeometry.Scheme.IdealSheafData.leOrdAlong_iff_forall_mem_of_upperSemicontinuous {X : Scheme} (I : X.IdealSheafData) (hI : UpperSemicontinuous fun (x : ↥X) => I.ord x) (Z : TopologicalSpace.Closeds ↥X) (m : ℕ∞) : I.LeOrdAlong Z m ↔ ∀ z ∈ Z, m ≤ I.ord z

Kollár's convention ord_Z I ≥ m for a closed Z that need not be irreducible (Hironaka/Scheme/IdealSheaf/Order/Along.lean), general form: it holds exactly when ord_z I ≥ m at every point of Z.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_le_ord_of_specializes {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] {η x : ↥X} (h : η ⤳ x) : I.ord η ≤ I.ord x

The order "does not increase under localization" ([Hau03, Appendix A]; the content of the upper semicontinuity): on a scheme smooth over a field of characteristic zero, ord_η I ≤ ord_x I when η specializes to x.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_le_ord_of_mem_closure {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] {η x : ↥X} (h : x ∈ closure {η}) : I.ord η ≤ I.ord x

In terms of closures: if x ∈ closure {η} then ord_η I ≤ ord_x I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlong_le_ord {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (Z : TopologicalSpace.IrreducibleCloseds ↥X) {z : ↥X} (hz : z ∈ Z) : I.ordAlong Z ≤ I.ord z

The generic point of Z has the smallest order on Z.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlong_eq_iInf {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (Z : TopologicalSpace.IrreducibleCloseds ↥X) : I.ordAlong Z = ⨅ z ∈ ↑Z, I.ord z

[Hau03, Appendix A]: ord_Z I = min_{z ∈ Z} ord_z I for an irreducible closed Z.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlong_eq_iInf_closedPoints {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (Z : TopologicalSpace.IrreducibleCloseds ↥X) : I.ordAlong Z = ⨅ z ∈ ↑Z ∩ closedPoints ↥X, I.ord z

[Hau03, Appendix A], "where it suffices to take the minimum over the closed points a of Z": a scheme locally of finite type over a field is a Jacobson space (Mathlib's LocallyOfFiniteType.jacobsonSpace).

theorem AlgebraicGeometry.Scheme.IdealSheafData.leOrdAlong_iff_forall_mem {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (Z : TopologicalSpace.Closeds ↥X) (m : ℕ∞) : I.LeOrdAlong Z m ↔ ∀ z ∈ Z, m ≤ I.ord z

Kollár's convention ord_Z I ≥ m for a closed Z that need not be irreducible holds exactly when ord_z I ≥ m at every point z of Z.