Constructibility and finiteness of the order function

[Kol07, Definition 47]: x ↦ ord_x I is a constructible and upper semicontinuous function on X, and max-ord_Z I := max{ord_z I : z ∈ Z}, max-ord I := max-ord_X I. [Hau03, Appendix A]: on a Noetherian scheme "the order of I takes only finitely many values", and [Hau03, Appendix B]: the finite stratification by the order, whose stratum of maximal value is closed, the top locus.

• {ord = m} = {ord ≥ m} \ {ord ≥ m + 1} (setOf_ord_eq_eq_sdiff) is the difference of two closed sets (Hironaka/Scheme/IdealSheaf/Order/Semicontinuity.lean), hence locally closed (isLocallyClosed_setOf_ord_eq) and, on a Noetherian space, constructible (isConstructible_setOf_ord_eq; IsClosed.isConstructible: the complement of a closed set is open and compact, hence retrocompact);
• the descending chain of closed sets {ord ≥ m} stabilizes, Closeds X being well-founded under < on a Noetherian space, at {ord = ∞} = ⋂_m {ord ≥ m} (exists_setOf_le_ord_eq_setOf_ord_eq_top), which is {x : I_x = 0} by Krull; so off {I_x = 0} the order is bounded by some m₀ (exists_ord_le_of_stalkIdeal_ne_bot) and takes finitely many values (finite_image_ord_setOf_stalkIdeal_ne_bot, finite_range_ord). "I nonzero on every irreducible component" is I_η ≠ 0 at each generic point η; the stalk ideal at a generization x ⤳ y is the extension of the one at y (stalkIdeal_specializes), so I_y = 0 forces I_η = 0 at the generic point of a component through y (stalkIdeal_eq_bot_of_specializes, stalkIdeal_ne_bot_of_irreducibleComponents) and the order is then finite everywhere (ord_ne_top_of_irreducibleComponents);
• maxOrd I := maxOrdAlong I univ; maxOrdAlong I Z = sSup (ord '' Z) (maxOrdAlong_eq_sSup_image) is attained on a nonempty Z with I_x ≠ 0 on Z, a nonempty finite set of ℕ∞ containing its supremum (exists_ord_eq_maxOrdAlong), and finite (maxOrdAlong_ne_top); likewise maxOrd (exists_ord_eq_maxOrd, maxOrd_ne_top, isGreatest_range_ord);
• topLocus I := {x : ord_x I = maxOrd I} equals {ord ≥ maxOrd I} (topLocus_eq_setOf_le), which is {ord = ∞} or some {ord ≥ m}, closed either way (isClosed_topLocus, no Noetherian hypothesis); every level set is constructible (isConstructible_preimage_ord) and there are finitely many (finite_range_ord_and_isConstructible_preimage_ord).

The hypotheses of the main theorems (Challenge/Algebraic.lean: quasi-compact and locally of finite type over a field) give IsNoetherian X (Scheme.Hom.isNoetherian_of_field), hence NoetherianSpace X by Mathlib.

Used for the maximal order throughout (Hironaka/Resolution/Algebraic/MaximalContact/Basic.lean, Hironaka/Resolution/Algebraic/Balanced/Order.lean, Hironaka/Scheme/IdealSheaf/Derivative/Properties.lean, Hironaka/Resolution/Algebraic/Hir64/MainTheoremIIN.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/Data.lean, Hironaka/Resolution/Algebraic/Wlo05/EmbeddedFunctor.lean, Hironaka/Resolution/Algebraic/BoundaryClearing/Basic.lean, among others).

theorem IsClosed.isConstructible {Y : Type u_1} [TopologicalSpace Y] [TopologicalSpace.NoetherianSpace Y] {s : Set Y} (hs : IsClosed s) : Topology.IsConstructible s

A closed set in a Noetherian space is constructible — its complement is open and, like every subset of a Noetherian space, compact, hence retrocompact.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.maxOrd {X : Scheme} (I : X.IdealSheafData) : ℕ∞

[Kol07, Definition 47]: max-ord I := max-ord_X I, the supremum of ord_x I over all points of X — maxOrdAlong on Set.univ. It is attained and finite on a Noetherian X with I_x ≠ 0 at every point (exists_ord_eq_maxOrd, maxOrd_ne_top).

Equations

• I.maxOrd = I.maxOrdAlong Set.univ

def AlgebraicGeometry.Scheme.IdealSheafData.topLocus {X : Scheme} (I : X.IdealSheafData) : Set ↥X

[Hau03, Appendix B]: the top locus {x : ord_x I = max-ord I}, the stratum of maximal order. It is closed (isClosed_topLocus).

Equations

• I.topLocus = {x : ↥X | I.ord x = I.maxOrd}

theorem AlgebraicGeometry.Scheme.IdealSheafData.setOf_ord_eq_eq_sdiff {X : Scheme} (I : X.IdealSheafData) (m : ℕ) : {x : ↥X | I.ord x = ↑m} = {x : ↥X | ↑m ≤ I.ord x} \ {x : ↥X | ↑(m + 1) ≤ I.ord x}

{ord = m} = {ord ≥ m} \ {ord ≥ m + 1}.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_specializes {X : Scheme} (I : X.IdealSheafData) {x y : ↥X} (h : x ⤳ y) : I.stalkIdeal x = Ideal.map (CommRingCat.Hom.hom (X.presheaf.stalkSpecializes h)) (I.stalkIdeal y)

The stalk at a generization: for x ⤳ y, I_x = I_y 𝒪_{X,x} — the stalk ideal at x is the extension of the stalk ideal at y along the specialization map 𝒪_{X,y} → 𝒪_{X,x} (both are the extension of I(U) from an affine U ∋ y, which contains x).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_eq_bot_of_specializes {X : Scheme} (I : X.IdealSheafData) {x y : ↥X} (h : x ⤳ y) (hy : I.stalkIdeal y = ⊥) : I.stalkIdeal x = ⊥

I_y = 0 implies I_x = 0 for every generization x ⤳ y.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_ne_bot_of_irreducibleComponents {X : Scheme} (I : X.IdealSheafData) (h : ∀ Z ∈ irreducibleComponents ↥X, ∀ (η : ↥X), IsGenericPoint η Z → I.stalkIdeal η ≠ ⊥) (x : ↥X) : I.stalkIdeal x ≠ ⊥

Kollár's hypothesis I ≠ 0 on a variety ([Kol07, Definition 47]), read on a reducible X as "nonzero on every irreducible component": if I is nonzero at the generic point of every irreducible component of X, then I_x ≠ 0 at every point — x lies on the component irreducibleComponent x, whose generic point η generizes x.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_ne_top_of_irreducibleComponents {X : Scheme} (I : X.IdealSheafData) [IsLocallyNoetherian X] (h : ∀ Z ∈ irreducibleComponents ↥X, ∀ (η : ↥X), IsGenericPoint η Z → I.stalkIdeal η ≠ ⊥) (x : ↥X) : I.ord x ≠ ⊤

If I is nonzero on every irreducible component of the locally Noetherian X, the order is finite everywhere (Krull's intersection theorem).

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrdAlong_eq_sSup_image {X : Scheme} (I : X.IdealSheafData) (Z : Set ↥X) : I.maxOrdAlong Z = sSup ((fun (x : ↥X) => I.ord x) '' Z)

max-ord_Z I is the supremum of the set of values {ord_z I : z ∈ Z}.

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrd_eq_iSup {X : Scheme} (I : X.IdealSheafData) : I.maxOrd = ⨆ (x : ↥X), I.ord x

max-ord I = sup_x ord_x I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_maxOrd {X : Scheme} (I : X.IdealSheafData) (x : ↥X) : I.ord x ≤ I.maxOrd

ord_x I ≤ max-ord I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrd_le_iff {X : Scheme} (I : X.IdealSheafData) {m : ℕ∞} : I.maxOrd ≤ m ↔ ∀ (x : ↥X), I.ord x ≤ m

max-ord I ≤ m ⟺ ord_x I ≤ m for every x.

theorem AlgebraicGeometry.Scheme.IdealSheafData.topLocus_eq_setOf_le {X : Scheme} (I : X.IdealSheafData) : I.topLocus = {x : ↥X | I.maxOrd ≤ I.ord x}

The top locus is {x : ord_x I ≥ max-ord I}.

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

The hypotheses of the main theorems give the Noetherian hypothesis ([Hau03, Appendix A], "all our schemes will be assumed to be noetherian"): a scheme quasi-compact and locally of finite type over a field is Noetherian, hence a Noetherian topological space (Mathlib's IsNoetherian.noetherianSpace).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isLocallyNoetherian_of_smoothOfRelativeDimension {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] : IsLocallyNoetherian X

A scheme smooth over a field is locally Noetherian (it is locally of finite type).

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

{ord = m} is locally closed — the difference of two closed sets.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isConstructible_setOf_ord_eq {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] (m : ℕ) : Topology.IsConstructible {x : ↥X | I.ord x = ↑m}

[Kol07, Definition 47]: {ord = m} is constructible on a Noetherian X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_setOf_le_ord_eq_setOf_ord_eq_top {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] : ∃ (m₀ : ℕ), ∀ (m : ℕ), m₀ ≤ m → {x : ↥X | ↑m ≤ I.ord x} = {x : ↥X | I.ord x = ⊤}

The descending chain of closed sets {ord ≥ m} stabilizes (Closeds X is well-founded under < on a Noetherian space), at {ord = ∞} = ⋂_m {ord ≥ m}.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_ord_le_of_stalkIdeal_ne_bot {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] : ∃ (m₀ : ℕ), ∀ (x : ↥X), I.stalkIdeal x ≠ ⊥ → I.ord x ≤ ↑m₀

On X ∖ {I_x = 0} the order is bounded by some m₀.

theorem AlgebraicGeometry.Scheme.IdealSheafData.finite_image_ord_setOf_stalkIdeal_ne_bot {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] : ((fun (x : ↥X) => I.ord x) '' {x : ↥X | I.stalkIdeal x ≠ ⊥}).Finite

[Hau03, Appendix A]: on X ∖ {I_x = 0} the order takes finitely many values.

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

The order takes finitely many values on X (∞ included).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_ord_eq_maxOrdAlong {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] {Z : Set ↥X} (hZ : Z.Nonempty) (hI : ∀ x ∈ Z, I.stalkIdeal x ≠ ⊥) : ∃ z ∈ Z, I.ord z = I.maxOrdAlong Z

max-ord_Z I is attained for Z nonempty with I_x ≠ 0 at all x ∈ Z — the set of values is finite and nonempty, so it contains its supremum.

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrdAlong_ne_top {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] {Z : Set ↥X} (hI : ∀ x ∈ Z, I.stalkIdeal x ≠ ⊥) : I.maxOrdAlong Z ≠ ⊤

max-ord_Z I is finite when I_x ≠ 0 at all x ∈ Z.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_ord_eq_maxOrd {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] [Nonempty ↥X] (hI : ∀ (x : ↥X), I.stalkIdeal x ≠ ⊥) : ∃ (x : ↥X), I.ord x = I.maxOrd

max-ord I is attained on a nonempty X with I_x ≠ 0 everywhere.

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrd_ne_top {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] (hI : ∀ (x : ↥X), I.stalkIdeal x ≠ ⊥) : I.maxOrd ≠ ⊤

max-ord I is finite when I_x ≠ 0 everywhere.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isGreatest_range_ord {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] [Nonempty ↥X] (hI : ∀ (x : ↥X), I.stalkIdeal x ≠ ⊥) : IsGreatest (Set.range fun (x : ↥X) => I.ord x) I.maxOrd

max-ord I is the greatest value of x ↦ ord_x I on a nonempty X with I_x ≠ 0 everywhere (the form in which Main Theorem II takes the maximal order d).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_topLocus {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] : IsClosed I.topLocus

[Hau03, Appendix B]: the top locus {ord = max-ord I} is closed — it is {ord ≥ max-ord I}, that is {ord = ∞} when max-ord I = ∞ and {ord ≥ m} when max-ord I = m.

theorem AlgebraicGeometry.Scheme.IdealSheafData.topLocus_nonempty {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] [Nonempty ↥X] (hI : ∀ (x : ↥X), I.stalkIdeal x ≠ ⊥) : I.topLocus.Nonempty

The top locus is nonempty on a nonempty Noetherian X with I_x ≠ 0 everywhere.

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

The level set {ord = ∞} is constructible (it is closed).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isConstructible_preimage_ord {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] (v : ℕ∞) : Topology.IsConstructible ((fun (x : ↥X) => I.ord x) ⁻¹' {v})

Every level set of x ↦ ord_x I is constructible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.finite_range_ord_and_isConstructible_preimage_ord {X : Scheme} (I : X.IdealSheafData) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] [TopologicalSpace.NoetherianSpace ↥X] : (Set.range fun (x : ↥X) => I.ord x).Finite ∧ ∀ (v : ℕ∞), Topology.IsConstructible ((fun (x : ↥X) => I.ord x) ⁻¹' {v})

[Kol07, Definition 47]: x ↦ ord_x I is a constructible function — it takes finitely many values and every level set is constructible.

The unit ideal sheaf has maximal order 0

theorem AlgebraicGeometry.maxOrd_top {X : Scheme} : ⊤.maxOrd = 0

The unit ideal sheaf has maximal order 0 (ord_top at every point); in the namespace of its users, Hironaka/Resolution/Algebraic/Stage/Base.lean and Hironaka/Resolution/Algebraic/Wlo05/EmbeddedNil.lean.