Ideal sheaves on a scheme: stalks, order, invertibility, colon

The operations on and predicates of Mathlib's ideal sheaves X.IdealSheafData of a scheme X that the library adds.

• The stalk J_x ⊆ 𝒪_{X,x} of an ideal sheaf at a point: the ideal generated by the germs at x of the sections of J over the affine opens containing x (Hironaka's J_x [Hir64, Ch. 0, §5, p. 142]). Every such open gives the same ideal, and the supremum over all of them makes the definition choice-free.
• IsNonzeroEverywhere J: Hironaka's "coherent sheaf of non-zero ideals" [Hir64, Main Theorem II], read stalkwise.
• The order of J at x: Hironaka's ν(J_x), the largest ν with J_x ⊆ 𝔪_x^ν [Hir64, Ch. 0, §4]; Kollár's ord_x J [Kol07, Definition 47]; valued in ℕ∞, so that the zero ideal has order ⊤.
• IsInvertible J: the closed subscheme of J is an effective Cartier divisor, J being generated on an affine neighbourhood of every point by a nonzerodivisor [TSPA, Tag 01WS]. Mathlib has no invertible ideal sheaves on schemes, so this local characterisation is the definition. On a locally Noetherian scheme it is equivalent to its stalkwise reading, every J_x generated by a nonzerodivisor of 𝒪_{X,x} (the standing assumption of Hironaka's Definition 2 [Hir64, Ch. 0, §5, Definition 2]): isInvertible_iff_forall_stalkIdeal_eq_span of Hironaka/Scheme/IdealSheaf/Invertible.lean.
• The colon ideal sheaf (I : K), the largest ideal sheaf whose sections over every affine open lie in the colon ideal (I(U) : K(U)), and the K-power torsion saturation ⋃ᵢ (I : Kⁱ) of I [Hau14, Definition 6.2]; [TSPA, Tag 080D]. The transforms of an ideal sheaf under a blow-up are built from them.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal {X : Scheme} (J : X.IdealSheafData) (x : ↥X) : Ideal ↑(X.presheaf.stalk x)

The stalk J_x ⊆ 𝒪_{X,x} of an ideal sheaf: the ideal generated by the germs at x of the sections of J over the affine opens containing x (every such open gives the same ideal, stalkIdeal_eq_map_germ; the supremum makes the definition choice-free) [Hir64, Ch. 0, §5, p. 142].

Equations

• J.stalkIdeal x = ⨆ (U : ↑X.affineOpens), ⨆ (hx : x ∈ ↑U), Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hx)) (J.ideal U)

def AlgebraicGeometry.Scheme.IdealSheafData.IsNonzeroEverywhere {X : Scheme} (J : X.IdealSheafData) : Prop

Hironaka's "coherent sheaf of non-zero ideals" [Hir64, Main Theorem II; Corollary 1], read stalkwise: J_x ≠ 0 at every point. On a non-singular scheme this is Kollár's "not zero on any irreducible component" [Kol07, Theorem 35].

Equations

• J.IsNonzeroEverywhere = ∀ (x : ↥X), J.stalkIdeal x ≠ ⊥

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.ord {X : Scheme} (I : X.IdealSheafData) (x : ↥X) : ℕ∞

[Kol07, Definition 47]: the order of the ideal sheaf I at the point x, the largest m with I_x ⊆ 𝔪_xᵐ in 𝒪_{X,x}, as an element of ℕ∞ (⊤ exactly when I_x = 0); Hironaka's ν(J_x) [Hir64, Ch. 0, §4].

Equations

• I.ord x = sSup {n : ℕ∞ | ∃ (m : ℕ), n = ↑m ∧ I.stalkIdeal x ≤ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ^ m}

def AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible {X : Scheme} (J : X.IdealSheafData) : Prop

An ideal sheaf J on X is invertible (its closed subscheme is an effective Cartier divisor [TSPA, Tag 01WS]; [Kol07, Warning 20]) if every point x has an affine open neighbourhood U and a nonzerodivisor f ∈ Γ(X, U) with J(U) = (f).

Equations

• J.IsInvertible = ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ f ∈ nonZeroDivisors ↑(X.presheaf.obj (Opposite.op ↑U)), J.ideal U = Ideal.span {f}

def AlgebraicGeometry.Scheme.IdealSheafData.colon {X : Scheme} (I K : X.IdealSheafData) : X.IdealSheafData

The colon ideal sheaf (I : K): the largest ideal sheaf whose sections over every affine open lie in the colon ideal (I(U) : K(U)); equivalently (le_colon_iff_mul_le) the largest J with J * K ≤ I.

Equations

• I.colon K = AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals fun (U : ↑X.affineOpens) => Submodule.colon (I.ideal U) ↑(K.ideal U)

def AlgebraicGeometry.Scheme.IdealSheafData.saturate {X : Scheme} (I K : X.IdealSheafData) : X.IdealSheafData

The K-power torsion saturation ⋃ᵢ (I : Kⁱ) of I [Hau14, Definition 6.2]; [TSPA, Tag 080D] (the sections supported on the divisor).

Equations

• I.saturate K = ⨆ (i : ℕ), I.colon (K ^ i)