Ideal sheaves are determined by their stalks: the stalk calculus

The stalk J_x ⊆ 𝒪_{X,x} of an ideal sheaf (stalkIdeal) is the image of J(U) under the germ map for any affine U ∋ x (stalkIdeal_eq_map_germ), and 𝒪_{X,x} is the localization of Γ(X, U) at the prime of x (Mathlib's IsAffineOpen.isLocalization_stalk). Since an inclusion of ideals holds as soon as it holds after localizing at every maximal ideal (Mathlib's Ideal.le_of_localization_maximal), an inclusion of ideal sheaves can be checked on stalks (le_of_stalkIdeal_le, ext_stalkIdeal), and on a Jacobson scheme at the closed points alone (le_of_forall_stalkIdeal_le_of_isClosed). The stalk is compatible with the operations used in the divisor calculus: products, powers, suprema, finite products, and the colon by an invertible ideal sheaf (stalkIdeal_colon_of_isInvertible, Mathlib's colon commutes with localization for finitely generated divisors, map_colon_of_fg).

These are the tools for computing saturations and orders of ideal sheaves on stalks throughout the blow-up sequences of the resolution.

Main declarations

• stalkIdeal_top, stalkIdeal_bot, stalkIdeal_mul, stalkIdeal_pow, ideal_iSup', stalkIdeal_iSup' / stalkIdeal_iSup, stalkIdeal_finset_prod, stalkIdeal_colon_le, stalkIdeal_colon_of_isInvertible, stalkIdeal_saturate_of_isInvertible.
• le_of_forall_stalkIdeal_le_of_isMaximal, le_of_stalkIdeal_le, le_of_forall_stalkIdeal_le_of_isClosed, ext_stalkIdeal. The last two but one and the last are one-line corollaries of le_of_stalkIdeal_le and ext_stalkIdeal of Hironaka.Scheme.BlowUp.Descent, kept under these names.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_top {X : Scheme} (x : ↥X) : ⊤.stalkIdeal x = ⊤

The stalk of the unit ideal sheaf is the unit ideal.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_bot {X : Scheme} (x : ↥X) : ⊥.stalkIdeal x = ⊥

The stalk of the zero ideal sheaf is zero.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_mul {X : Scheme} (I J : X.IdealSheafData) (x : ↥X) : (I * J).stalkIdeal x = I.stalkIdeal x * J.stalkIdeal x

The stalk of a product is the product of the stalks.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_pow {X : Scheme} (I : X.IdealSheafData) (n : ℕ) (x : ↥X) : (I ^ n).stalkIdeal x = I.stalkIdeal x ^ n

The stalk of a power is the power of the stalk.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup' {X : Scheme} {ι : Sort u_1} (I : ι → X.IdealSheafData) : (⨆ (i : ι), I i).ideal = ⨆ (i : ι), (I i).ideal

Mathlib's ideal_iSup for a Sort-indexed supremum (a bounded supremum ⨆ i ∈ s is one).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_iSup' {X : Scheme} {ι : Sort u_1} (I : ι → X.IdealSheafData) (x : ↥X) : (⨆ (i : ι), I i).stalkIdeal x = ⨆ (i : ι), (I i).stalkIdeal x

The stalk of a Sort-indexed supremum is the supremum of the stalks.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_iSup {X : Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) (x : ↥X) : (⨆ (i : ι), I i).stalkIdeal x = ⨆ (i : ι), (I i).stalkIdeal x

The stalk of a supremum is the supremum of the stalks (the Type-indexed instance of stalkIdeal_iSup').

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_finset_prod {X : Scheme} {ι : Type u_1} (s : Finset ι) (g : ι → X.IdealSheafData) (x : ↥X) : (∏ i ∈ s, g i).stalkIdeal x = ∏ i ∈ s, (g i).stalkIdeal x

The stalk of a finite product of ideal sheaves is the product of the stalks (stalkIdeal_mul iterated; the empty product is the unit ideal, stalkIdeal_top).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_colon_le {X : Scheme} (I K : X.IdealSheafData) (x : ↥X) : (I.colon K).stalkIdeal x ≤ Submodule.colon (I.stalkIdeal x) ↑(K.stalkIdeal x)

The stalk of a colon is contained in the colon of the stalks.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_colon_of_isInvertible {X : Scheme} (I : X.IdealSheafData) {K : X.IdealSheafData} (hK : K.IsInvertible) (x : ↥X) : (I.colon K).stalkIdeal x = Submodule.colon (I.stalkIdeal x) ↑(K.stalkIdeal x)

For an invertible K the stalk of the colon is the colon of the stalks (the colon by a finitely generated ideal commutes with localization).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_saturate_of_isInvertible {X : Scheme} (I : X.IdealSheafData) {K : X.IdealSheafData} (hK : K.IsInvertible) (x : ↥X) : (I.saturate K).stalkIdeal x = ⨆ (i : ℕ), Submodule.colon (I.stalkIdeal x) ↑(K.stalkIdeal x ^ i)

For an invertible K the stalk of the saturation ⋃ᵢ (I : Kⁱ) is the saturation of the stalks.

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_forall_stalkIdeal_le_of_isMaximal {X : Scheme} {I J : X.IdealSheafData} (h : ∀ (U : ↑X.affineOpens) (P : Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) (hP : P.IsMaximal), I.stalkIdeal ((IsAffineOpen.fromSpec ⋯) { asIdeal := P, isPrime := ⋯ }) ≤ J.stalkIdeal ((IsAffineOpen.fromSpec ⋯) { asIdeal := P, isPrime := ⋯ })) : I ≤ J

The core of le_of_stalkIdeal_le: an inclusion of ideal sheaves holds as soon as it holds at the stalks of the points hU.fromSpec ⟨P⟩ of the MAXIMAL ideals P of Γ(X, U), U affine — 𝒪_{X,x} is the localization of Γ(X, U) at the prime of x for an affine U ∋ x, and an inclusion of ideals holds after localizing at every maximal ideal (Mathlib's Ideal.le_of_localization_maximal).

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_forall_stalkIdeal_le_of_isClosed {X : Scheme} [JacobsonSpace ↥X] {I J : X.IdealSheafData} (h : ∀ (x : ↥X), IsClosed {x} → I.stalkIdeal x ≤ J.stalkIdeal x) : I ≤ J

The closed-point form of le_of_stalkIdeal_le: on a Jacobson scheme — every scheme locally of finite type over a field, Mathlib's LocallyOfFiniteType.jacobsonSpace — an inclusion of ideal sheaves can be checked at the closed points: the maximal ideals of Γ(X, U), U affine, are the closed points of Spec Γ(X, U), and a closed point of an open subset of a Jacobson space is closed in the space (Topology.IsOpenEmbedding.preimage_closedPoints).