The chart membership criterion #
A point x of the affine blow-up B = affineBlowUp I lies in the chart of a ∈ I iff the image
of a in 𝒪_{B,x} generates the stalk of the exceptional ideal I·𝒪_B at x
[TSPA, Tag 0BFL]. The printed proof invokes the universal property; the proof here proceeds from
the chart overlaps and cancellation instead, so that the universal property
(Hironaka.Scheme.BlowUp.AffineBlowUp.Universal.Kernel, Uniqueness) can use the criterion.
The argument. Every x is chart b x' for some b ∈ I and a point x' of Spec R[I/b]. The
open immersion j = chart b identifies the stalks, so everything is computed in
𝒪_{Spec R[I/b], x'}, a localization of R[I/b] at the prime x':
- the stalk of the exceptional ideal at
xcorresponds to the stalk of(exceptionalIdeal I).comap j = ofIdealTop (b)(affineBlowUp.comap_exceptionalIdeal_chart), generated by the germ ofb, a nonzerodivisor (nonzerodivisors ofR[I/b]stay nonzerodivisors in its localizations); - the image of
acorresponds to the germ ofa ∈ R[I/b], anda = b · (a/b)there (algebraMap_eq_mul_ratio); x = j x'lies in the chart ofaiffx' ∈ D(a/b)(affineBlowUp.chart_preimage_chart) iff the germ ofa/bis a unit (Scheme.mem_basicOpen_top,basicOpen_eq_of_affine).
Hence (a) = (b) at x iff a/b is a unit at x: if a/b is a unit, (b · (a/b)) = (b); if
(b · (a/b)) = (b) with b a nonzerodivisor, a/b is a unit (cancellation,
isUnit_of_span_mul_eq_span). The chart overlaps U_a ∩ U_b = D(a/b) are the gluing data of
[Hau14, Definition 4.13]; the description of the stalks of the blow-up as localizations of the
chart rings is the local blow-up of [Hau14, Definitions 4.15 and 4.16]. The transport lemmas of
the first section are bookkeeping for affine schemes.
On an affine scheme, the ideal of ofIdealTop J on the affine open ⊤ is J.
On an affine scheme, the stalk of ofIdealTop J at x is generated by the germs of J.
On an affine scheme, the ideal sheaf of a principal ideal generated by a nonzerodivisor of the
global sections is invertible (the definition of IsInvertible with the affine open ⊤).
The germ at a point x of Spec S of an element s ∈ S, read as a global section through
ΓSpecIso: the canonical map S → 𝒪_{Spec S, x}.
Equations
Instances For
The germ of s at x is a unit iff x lies in the basic open of s (Mathlib's
mem_basicOpen_top; basicOpen_eq_of_affine identifies it with PrimeSpectrum.basicOpen s).
A nonzerodivisor of Γ(Spec S, ⊤) has a nonzerodivisor germ at every point: the stalk is a
localization of the global sections (Mathlib's isLocalization_stalk).
(Spec.map φ)♯ on global sections, applied to ΓSpecIso.inv r, is ΓSpecIso.inv (φ r).
The stalk map of Spec.map φ at x sends the germ of r to the germ of φ r.
a = b · (a/b) in R[I/b], for a, b ∈ I.
At a point x' of the chart of b, the stalk of the exceptional ideal (pulled back to the
chart) is generated by the germ of b.
The image of r ∈ R in 𝒪_{B, chart b x'}, transported to the chart's stalk by the
isomorphism (chart b).stalkMap x', is the germ of r ∈ R[I/b] (from chart ≫ π = Spec (R → R[I/b]), affineBlowUp.chart_π).
At a point x' of the chart of b, the stalk of the exceptional ideal, read in the stalk of
Spec R[I/b] through the chart's stalk map (an isomorphism), is generated by the germ of b —
stalkIdeal_comap_exceptionalIdeal_chart in map form.
The stalk of the affine blow-up at a point x' of the chart of b is the localization
R[I/b]_{x'}, compatibly with germs (Mathlib's Spec.stalkIso through the chart's stalk map, an
isomorphism): the local blow-up of [Hau14, Definitions 4.15 and 4.16].
The stalk of the exceptional ideal at chart b x' is generated by the image of a ∈ R iff,
in the chart's stalk, the germs of b and of a generate the same ideal.
Inside the chart of b, the chart of a is the basic open of the global section a/b of
Spec R[I/b] (affineBlowUp.chart_preimage_chart in the scheme's vocabulary).
The chart membership criterion [TSPA, Tag 0BFL]: a point x of the affine blow-up lies in
the chart of a ∈ I iff the image of a in 𝒪_{B,x} generates the stalk of the exceptional
ideal at x. Proved from the chart overlaps and cancellation rather than from the universal
property.
The relative form of the criterion: at a point x of the chart of b, the image of a is
the image of b times a factor u (the transport of a/b ∈ R[I/b] to 𝒪_{B,x}), and x lies
in the chart of a as soon as u is a unit.