Invertibility of an ideal sheaf read at the stalks

An ideal sheaf J on a scheme is invertible (IdealSheafData.IsInvertible, an effective Cartier divisor [TSPA, Tag 01WS]) when near every point it is generated on an affine open by a nonzerodivisor. This module relates that definition to the stalks.

• IsInvertible.exists_ne_zero_stalkIdeal_eq_span: the stalk of an invertible ideal sheaf is generated by a nonzero element (the germ of the local nonzerodivisor generator is nonzero in the localization); the nonzerodivisor form is IsInvertible.exists_mem_nonZeroDivisors_stalkIdeal_eq_span of Hironaka/Scheme/IdealSheaf/StalkIdeal.lean. A nonzero generator is what the order computations along a blow-up sequence use.
• isInvertible_of_forall_stalkIdeal_eq_span, isInvertible_iff_forall_stalkIdeal_eq_span: on a locally Noetherian scheme the converse holds, so invertibility is the stalkwise condition "every stalk is generated by a nonzerodivisor of 𝒪_{X,x}" (the standing assumption of Hironaka's Definition 2 [Hir64, Ch. 0, §5, Definition 2]; [Kol07, Warning 20]). This is the form in which the invertibility of a centre or of a reduced snc divisor is checked. The argument is routine commutative algebra, not stated as such in the sources.

Spreading out a generator. Let A be a Noetherian ring, J ⊆ A an ideal, p a prime, S = A_p, and a ∈ J with J S = (a) and a a nonzerodivisor of S. For each of the finitely many generators g of J we have g/1 ∈ (a/1), so s_g g ∈ (a) for some s_g ∉ p (Ideal.exists_mul_mem_span_of_mem_map); the annihilator of a is finitely generated and each of its generators dies in S, so it is killed by some s' ∉ p (Ideal.exists_mul_eq_zero_of_mem_nonZeroDivisors). On A_s with s = s' ∏ s_g the ideal J A_s is (a) (each g is a unit multiple of an element of (a)) and a is a nonzerodivisor (a relation z a = 0 in A_s lifts to y a = 0 up to a power of s, so y lies in the annihilator, so s' y = 0 and z = 0): that is the datum IsRegularGeneratorIn (Localization.Away s) a (Ideal.exists_isRegularGeneratorIn_away).

On a scheme. For a locally Noetherian X and an ideal sheaf J whose stalk at every point is generated by a nonzerodivisor, every affine open U and prime p of Γ(U) give the point x = fromSpec p ∈ U, whose stalk is the localization of Γ(U) at p (Mathlib's IsAffineOpen.isLocalization_stalk') and whose stalk ideal is the extension of J(U); a generator a of the stalk ideal is a unit multiple of the image of an element of J(U), and the ring lemma gives the datum at p. Hence J(U) is invertible for every affine U, i.e. J is invertible.

theorem Ideal.exists_mul_mem_span_of_mem_map {A : Type u} [CommRing A] (p : Ideal A) [p.IsPrime] (S : Type v) [CommRing S] [Algebra A S] [IsLocalization.AtPrime S p] {a g : A} (hg : (algebraMap A S) g ∈ span {(algebraMap A S) a}) : ∃ s ∉ p, s * g ∈ span {a}

Spreading a generator: if g/1 ∈ (a/1) in the localization at p, then s g ∈ (a) for some s ∉ p.

theorem Ideal.exists_mul_eq_zero_of_mem_nonZeroDivisors {A : Type u} [CommRing A] (p : Ideal A) [p.IsPrime] (S : Type v) [CommRing S] [Algebra A S] [IsLocalization.AtPrime S p] [IsNoetherianRing A] {a : A} (ha : (algebraMap A S) a ∈ nonZeroDivisors S) : ∃ s ∉ p, ∀ (c : A), c * a = 0 → s * c = 0

Spreading a nonzerodivisor: if a/1 is a nonzerodivisor of the localization at p and A is Noetherian, some s ∉ p kills the annihilator of a.

theorem Ideal.exists_isRegularGeneratorIn_away {A : Type u} [CommRing A] (p : Ideal A) [p.IsPrime] (S : Type v) [CommRing S] [Algebra A S] [IsLocalization.AtPrime S p] [IsNoetherianRing A] (J : Ideal A) {a : A} (haJ : a ∈ J) (hmap : map (algebraMap A S) J = span {(algebraMap A S) a}) (hnzd : (algebraMap A S) a ∈ nonZeroDivisors S) : ∃ s ∉ p, J.IsRegularGeneratorIn (Localization.Away s) a

The datum IsRegularGeneratorIn at a prime, from the localization at that prime: if a ∈ J generates J A_p and is a nonzerodivisor of A_p, then for some s ∉ p it generates J A_s and is a nonzerodivisor of A_s.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.exists_ne_zero_stalkIdeal_eq_span {X : Scheme} {K : X.IdealSheafData} (hK : K.IsInvertible) (x : ↥X) : ∃ (g : ↑(X.presheaf.stalk x)), g ≠ 0 ∧ K.stalkIdeal x = Ideal.span {g}

The stalk of an invertible ideal sheaf is principal with a nonzero generator — the germ of a local nonzerodivisor generator is nonzero in the localization: if f/1 = 0 in the stalk then s f = 0 for some s outside the prime of the point, so s = 0, contradicting s ∉ 𝔭.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_of_forall_stalkIdeal_eq_span {X : Scheme} [IsLocallyNoetherian X] (J : X.IdealSheafData) (h : ∀ (x : ↥X), ∃ a ∈ nonZeroDivisors ↑(X.presheaf.stalk x), J.stalkIdeal x = Ideal.span {a}) : J.IsInvertible

On a locally Noetherian scheme an ideal sheaf whose stalk at every point is generated by a nonzerodivisor is invertible (an effective Cartier divisor, [TSPA, Tag 01WS]; the center of a trivial blow-up, [Kol07, Warning 20]): on every affine open the ideal is invertible, the datum at each prime coming from the stalk at the corresponding point by spreading out.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_iff_forall_stalkIdeal_eq_span {X : Scheme} [IsLocallyNoetherian X] (J : X.IdealSheafData) : J.IsInvertible ↔ ∀ (x : ↥X), ∃ a ∈ nonZeroDivisors ↑(X.presheaf.stalk x), J.stalkIdeal x = Ideal.span {a}

On a locally Noetherian scheme, invertibility of an ideal sheaf is the stalkwise condition: every stalk is generated by a nonzerodivisor of the local ring (the standing assumption of Hironaka's Definition 2 [Hir64, Ch. 0, §5, Definition 2]).