Bierstone–Milman's Proposition 3.13: the reduction to the chart ring #
At every point a' of the blowing-up π : M' → M of M with centre Y, the saturation
⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) of the total transform of a coherent ideal I, the stalk of the
strict transform X', is the ideal generated by the strict transforms y^{-d}(f ∘ π) of the
elements f ∈ I_{π(a')} (strictTransformElems): [BM97, Proposition 3.13]. Bierstone–Milman
prove this with the diagram of initial exponents and Hironaka's division theorem; the proof here
takes a different route, through the flatness of the completion of the chart ring (the printed
argument's truncation step, which passes through the order of Lemma 3.22, is not reproduced):
- In a blow-up chart of index
iata'overY, the chart-ring mapχ : R' → 𝒪_{M',a'}ofHironaka.Manifold.BlowUp.Transform.KollarChart(Kollár's chart Kol07, Definition 60, (60.2); here in the general formIsLocalRing.exists_chartRing_hom_of_mul_eq, for the coordinates shifted ata'; the coordinate permutationτisexists_kollarPerm) identifies the total transform's stalk withχ(I_a R')(IdealSheaf.stalkIdeal_pullback) and the exceptional ideal with(χ(x_r))(stalkIdeal_exceptionalIdealSheaf_eq_span_coord), so the saturation is⋃_k (χ(I_a R') : χ(x_r)^k). - Given a flat descent datum for
χ(Algebra.HasFlatDescentDatum: a ringTwith𝒪_{M',a'} → Talong which ideals descend andR' → Tflat; the completionT = 𝒪̂_{M',a'},Hironaka.Manifold.BlowUp.Transform.StrictSubspaceCompletion), this isχ(⋃_k (I_a R' : x_r^k))(Algebra.iSup_colon_pow_map_eq_map_iSup_colon_pow), and the chart-ring saturation is the ideal of the transformsx_r^{-M} φ(f),f ∈ I_a(Hironaka.Algebra.Local.ChartSaturation). - A transform
gwithx_r^M g = φ(f)maps toχ(g)withχ(x_r)^M χ(g) = f ∘ π: a strict transform off(map_transformsIdeal_le_span_strictTransformElems); conversely every strict transform lies in the saturation (span_strictTransformElems_le_saturationStalk). - Off the centre (
π(a') ∉ Y) the exceptional ideal is the unit ideal, the saturation is the total transform (saturationStalk_of_notMem_cosupport) andf ∘ π = 1^0 · (f ∘ π)is a strict transform (saturationStalk_eq_span_strictTransformElems_of_notMem).
Hironaka.Manifold.BlowUp.Transform.StrictSubspaceCompletion supplies the flat descent datum
(the completion identification 𝒪̂_{M',a'} ≅ (R'_{𝔪'})^ through Cohen's structure theorem) and
assembles the proposition at every a' (saturationStalk_eq_span_strictTransformElems). Nothing
is assumed of I: I = ⊤ and I = ⊥ are covered (⊤: every element is a strict transform of
itself with d = 0; ⊥: both sides are ⊥). Hironaka describes the strict transform as the
union of the kernels ⋃_n (g⁻¹I : (g^*J)^n) [Hir64, Ch. 0, §2, pp. 129–130].
χ is a chart-ring map at a' for the blow-up chart Φ of index i over the adapted
chart φ, at a point over the centre, with the coordinates x indexed through the permutation
τ (Kollár's convention: τ r = σ i is the scaling coordinate and the τ j, j < r, are the
other centre coordinates): χ ∘ φ_R = germMap π, x_j / x_r ↦ u_{τ j} − u_{τ j}(a') (j < r:
the ratio coordinates centred at a', so that χ⁻¹(𝔪_{a'}) is the chart origin of x — the
form exists_chartRing_hom takes when the coordinates x are Kollár's coordinates
kollarCoords shifted at a') and x_r ↦ u_{σ i}.
- algebraMap_eq (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))) : χ ((algebraMap ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) ↥(IsLocalRing.chartRing x r)) s) = (germMap π ⋯ a') s
- xr_eq : χ ((algebraMap ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) ↥(IsLocalRing.chartRing x r)) (x r)) = coord E ψ Φ ⋯ ha' (σ i)
Instances For
Through a chart-ring map χ compatible with the germ map, the total transform's stalk is the
image of the extension I_a R' (IdealSheaf.stalkIdeal_pullback, rewritten through
χ ∘ φ_R = germMap π).
BM97 Prop 3.13, the transport (flatness route): in a blow-up chart at a' over
Y, given a flat descent datum for the chart-ring map χ, the saturation of the total transform
is the image under χ of the ideal of the transforms x_r^{-M} φ(f), f ∈ I_{π(a')}, of the chart
ring.
BM97 Prop 3.13, the easy inclusion in the chart: the image under χ of a transform g,
x_r^M g = φ(f) with f ∈ I_{π(a')}, is a strict transform of f —
u_{σ i}^M χ(g) = f ∘ π with (u_{σ i}) = I_{F,a'}.
BM97 Prop 3.13 at a point over the centre (flatness route), given a flat descent
datum for the chart-ring map: the saturation is generated by the strict transforms of the
elements of I_{π(a')}.
BM97 Prop 3.13 off the centre: at a' with π(a') ∉ Y the exceptional ideal is the unit
ideal, the saturation is the total transform's stalk, and every f ∘ π is the strict transform
1^0 · (f ∘ π) of f.
The centred adapted coordinates at π(a'), permuted by τ: x_j = u_{τ j} - u_{τ j}(π a'),
the coordinate family exists_chartRing_hom takes.
Equations
- Manifold.centredCoords hφ hΦ ha' τ j = Manifold.coord E ψ φ ⋯ ⋯ (τ j) - (Manifold.const 𝕜 E M (π a')) ((Manifold.eval 𝕜 E M (π a')) (Manifold.coord E ψ φ ⋯ ⋯ (τ j)))