The order of an ideal sheaf at a point

[Kol07, Definition 47]: for an ideal sheaf I on a scheme X and a point x, ord_x I := max {r : 𝔪_xʳ 𝒪_{X,x} ⊇ I 𝒪_{X,x}}, the order of vanishing of I at x; [Hau03, Appendix A]: the order of I at a is the maximal power of 𝔪_a containing the stalk I_a, and "the zero ideal has infinite order". Here I_x = stalkIdeal I x ⊆ 𝒪_{X,x} is the stalk of the ideal sheaf and the order ord I x is valued in ℕ∞.

• ord I x is Hironaka's order ν(J_x), in which the main theorems are stated. It is the order of the ideal I_x in the local ring 𝒪_{X,x} (IsLocalRing.ord; ord_eq_ord_stalkIdeal, le_ord_iff).
• ord_x I = ∞ iff I_x = 0 (Krull's intersection theorem in the Noetherian local ring 𝒪_{X,x}, through ord_eq_top_iff of Hironaka/Algebra/Local/Order.lean); ord_x I = 0 iff x ∉ V(I) = Supp 𝒪/I; ord_x I ≥ 1 iff x ∈ V(I). The link is mem_support_iff_stalkIdeal_le_maximalIdeal: x lies in the support exactly when the stalk ideal is proper, every section of I over an affine neighbourhood being a non-unit at x (Mathlib's mem_zeroLocus_iff, Scheme.mem_basicOpen).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_eq_ord_stalkIdeal {X : Scheme} (I : X.IdealSheafData) (x : ↥X) : I.ord x = IsLocalRing.ord (I.stalkIdeal x)

The order at x is the order (IsLocalRing.ord) of the stalk ideal I_x in the local ring 𝒪_{X,x}.

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_ord_iff {X : Scheme} (I : X.IdealSheafData) (x : ↥X) {r : ℕ} : ↑r ≤ I.ord x ↔ I.stalkIdeal x ≤ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ^ r

Kollár's defining property ([Kol07, Definition 47]): r ≤ ord_x I iff I_x ⊆ 𝔪_xʳ.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_anti {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (x : ↥X) : J.ord x ≤ I.ord x

The order is antitone in the ideal sheaf.

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_stalkIdeal_le_maximalIdeal {X : Scheme} (I : X.IdealSheafData) (x : ↥X) : x ∈ I.support ↔ I.stalkIdeal x ≤ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)

A point lies in the support V(I) exactly when the stalk ideal is proper, i.e. contained in the maximal ideal of 𝒪_{X,x}: every section of I over an affine neighbourhood is a non-unit at x (Mathlib's mem_zeroLocus_iff and Scheme.mem_basicOpen).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_eq_zero_iff {X : Scheme} (I : X.IdealSheafData) (x : ↥X) : I.ord x = 0 ↔ x ∉ I.support

The order vanishes exactly off the support V(I) = Supp 𝒪_X/I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.one_le_ord_iff {X : Scheme} (I : X.IdealSheafData) (x : ↥X) : 1 ≤ I.ord x ↔ x ∈ I.support

ord_x I ≥ 1 exactly on the support V(I).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_eq_top_iff {X : Scheme} (I : X.IdealSheafData) (x : ↥X) [IsLocallyNoetherian X] : I.ord x = ⊤ ↔ I.stalkIdeal x = ⊥

"The zero ideal has infinite order" ([Hau03, Appendix A]; Krull's intersection theorem in the Noetherian local ring 𝒪_{X,x}): ord_x I = ∞ iff I_x = 0.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_top {X : Scheme} (x : ↥X) : ⊤.ord x = 0

The order of the unit ideal sheaf is 0 everywhere.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_bot {X : Scheme} (x : ↥X) : ⊥.ord x = ⊤

The order of the zero ideal sheaf is ∞ everywhere.