Colon and saturation of ideal sheaves; transforms under a blow-up #
The transforms of an ideal sheaf under a blow-up — total, strict, controlled and weak
[Hau14, Definitions 6.1, 6.2 and 6.8]; [Hir64, Ch. 0, §5, p. 142] — are built from two operations on
ideal sheaves: the colon ideal sheaf (I : K) (IdealSheafData.colon) and the K-power torsion
saturation ⋃ᵢ (I : Kⁱ) (IdealSheafData.saturate); they are defined along any morphism
π : B ⟶ X with a distinguished ideal sheaf E on B (strictTransformAlong π E J,
controlledTransformAlong π E J c, exceptionalOrderAlong π E J, weakTransformAlong π E J), the
blow-up and its exceptional divisor in the applications. This module proves the calculus of the
two operations and the elementary properties of the transforms, and defines Kollár's birational
transform of a marked ideal under the blow-up with centre D, J.markedTransform D m
[Kol07, Definition 60], the controlled transform along D.blowUpπ with control m.
Main declarations #
le_colon_iff_mul_le:(I : K)is the largest ideal sheafJwithJ * K ≤ I; its sections on an affine open are the colon ideal(I(U) : K(U))whenever everyK(U)is finitely generated (ideal_colon_of_fg), in particular forKinvertible (ideal_colon_of_isInvertible, viaIdeal.IsInvertible.fg).ideal_saturate,coe_support_saturate: the sections and the support of the saturation.pow_mul_colon_of_dvd:E ^ c * (I : E ^ c) = IwhenE ^ c ∣ I;colon_pow_eq_of_mul_eq: for invertibleEthe quotient is unique.controlledTransformAlong_le_strictTransformAlong,ideal_controlledTransformAlong_of_appLE: the controlled transforms lie below the strict transform; the chart formula.IdealSheafData.markedTransform J D m.
The arguments #
Colon and localization. For a finitely generated ideal J = (j₁, …, jₙ) of R and a
localization S of R at M, (I : J) S = (I S : J S) (map_colon_of_fg): the inclusion ⊆
is formal; for ⊇, an element z = x/m with z jₖ ∈ I S for every k has cₖ x jₖ ∈ I for some
cₖ ∈ M, so c x ∈ (I : J) for c = ∏ cₖ and z = (c x)/(c m). Hauser's Lemma 6.3 is the
case of a principal J.
Finite generation of invertible ideals. An invertible ideal J of A is generated, on a
basic open D(s) around each prime, by one element a ∈ J; finitely many such D(sₖ) cover
Spec A; for x ∈ J some power sₖ^N x lies in (aₖ) for every k, and the sₖ^N generate
the unit ideal, so J = (a₁, …, aₙ).
Uniqueness of the quotient. If E ^ c * K = I with E invertible then K ≤ (I : E ^ c) by
definition, and conversely on an affine open where E ^ c is generated by a nonzerodivisor e,
u e ∈ e K forces u ∈ K; such opens cover the scheme.
Conventions #
The colon of ideals is Mathlib's Submodule.colon with the divisor coerced to a set:
(I.ideal U).colon (K.ideal U : Set Γ(X, U)). The exceptional order is a natural number: the
supremum in ℕ of the exponents c with E ^ c ∣ J.comap π (0 when unbounded, i.e. when
J.comap π = 0, and 0 when only c = 0 qualifies).
Boundary cases #
K = ⊤: (I : ⊤) = I, the saturation is I. K = ⊥: (I : ⊥) = ⊤. I = ⊤: every colon is
⊤. J.comap π = 0: the exceptional order is 0 and the weak transform is 0. c = 0: the
controlled transform is the total transform.
Ring-level lemmas #
J ≤ (I : K) iff J K ≤ I, for ideals.
The colon by a finitely generated ideal commutes with localization, (I : J) S = (I S : J S)
(the case of a principal divisor is [Hau14, Lemma 6.3]).
An invertible ideal is finitely generated: it is principal on finitely many basic opens covering the spectrum, and the generators, together with the covering relation, generate it.
For f : R → S, an ideal I ⊆ R and s ∈ R, ⋃ᵢ (Iᵉ : f(s)ⁱ) = (I·R_s)ᵉ ∩ S: the extension
of I·R_s along f_s : R_s → S_{f(s)}, pulled back to S [Hau14, Lemma 6.3]. Hauser's
computation: u f(s)ⁱ = ∑ aⱼ f(xⱼ) iff u = ∑ aⱼ f(xⱼ/sⁱ).
The ring form of "for principal ideals the weak and strict transforms coincide"
[Hau14, Remark 6.9]: in a domain, for a prime h not dividing g, ⋃ᵢ ((hᵏ g) : hⁱ) = (g).
The colon of ideal sheaves #
((I : K) : L) = (I : K L).
On every affine open the sections of the colon sheaf are the colon ideal, provided the divisor
is finitely generated on every affine open: the family U ↦ (I(U) : K(U)) is then itself an ideal
sheaf (AlgebraicGeometry.map_colon_of_fg), and colon recovers it.
The power-torsion saturation #
If I is K-saturated, (I : K) = I, then every colon (I : K^i) is I and the saturation
is I itself.
The colon formula on a chart [Hau14, Definition 6.2]: for an invertible K generated on the
affine open U by e, the saturation has sections ⋃ᵢ (I(U) : eⁱ).
Division by an invertible power #
For invertible E, the quotient of I by E ^ c is unique: E ^ c * K = I → K = (I : E ^ c).
The support of the saturation #
A point fromSpec q of the affine open U lies in the zero locus of s ⊆ Γ(X, U) iff
s ⊆ q.
For x in the affine open U with prime 𝔭 = primeIdealOf x, x lies in the zero locus of
s ⊆ Γ(X, U) iff s ⊆ 𝔭.
On a locally Noetherian scheme the underlying set of V((I : K^∞)) is the closure of
V(I) ∖ V(K): the strict transform is the closure of the part off the exceptional divisor
[Hau14, Definition 6.2]; [TSPA, Tag 080D].
Transforms along a morphism with a distinguished divisor #
The chart formula for the controlled transform [Kol07, Definition 60, (60.2)–(60.3)]: on an
affine open U' of B over an affine open U of X on which the invertible divisor E is
generated by the pullback of a ∈ Γ(X, U), the controlled transform with control m has
sections (J(U)·Γ(U') : (π♯a)ᵐ) (the total transform's sections are J(U)·Γ(U'),
ideal_comap_of_le).
The marked transform under a blow-up #
Kollár's birational transform of the marked ideal (J, m) under the blow-up with centre D,
π_*^{-1}(J, m) = (𝒪(mF) · π^* J, m) [Kol07, Definition 60, (60.1)]: the controlled transform
of J with control m along D.blowUpπ with respect to the exceptional divisor
F = D.exceptionalDivisor. Kollár defines it for m ≤ ord_D J; the colon ideal
(π^* J : F^m) is defined for every J and m, and satisfies F^m · π_*^{-1}(J, m) = π^* J
exactly when F^m divides π^* J. The mark m is carried alongside the ideal
(MarkedTriple).
Equations
- J.markedTransform D m = J.controlledTransformAlong D.blowUpπ D.exceptionalDivisor m