The lift of a derivation to the chart of a blow-up: the construction #
Włodarczyk's proof of [Wlo05, Lemma 2.6.3]: "any derivation D of 𝒪_X induces a derivation
y σ^*(D) of 𝒪_{X'}", y the local equation of the exceptional divisor. In the local model
of Hironaka/Algebra/Local/ChartRing.lean (R a commutative ring, x : Fin n → R, the centre
P = ⟨x₀, …, x_r⟩, the chart ring R' = R[xᵢ/x_r : i < r] ⊆ R[1/x_r], y = x_r), a
k-derivation δ of R extends to R[1/x_r] by the quotient rule
(Derivation.localization), and x_r · δ̃ preserves R': on the generators yⱼ = xⱼ/x_r the
Leibniz rule for yⱼ · x_r = xⱼ gives x_r · δ̃(yⱼ) = δ(xⱼ) − yⱼ · δ(x_r) ∈ R' (the table of
derivatives in Włodarczyk's proof), on the image of R it is x_r · δ(a), and R' is closed
under sums and Leibniz products (Algebra.adjoin_induction, as for the coordinate derivations in
Hironaka/Algebra/Local/Chart.lean). The restriction Derivation.blowupLift δ is Włodarczyk's
y σ^*(D); coe_blowupLift is its defining identity. The exceptional identity D'(y) ∈ (y),
the transform identity π⁻¹_*(δ f, m) = D'(π⁻¹_*(f, m+1)) + (m+1) δ(x_r) π⁻¹_*(f, m+1) and the
inclusion π⁻¹_*(D(I), m) ⊆ D(π⁻¹_*(I, m+1)) are proved in
Hironaka/Algebra/Local/BlowUpLiftTransform.lean; the logarithmic variant is in
Hironaka/Algebra/Local/BlowUpLiftLog.lean.
For the coordinate derivations ∂ᵢ this lift is the x_r ∂ᵢ of
Hironaka/Algebra/Local/TransformDeriv.lean (smul_awayPderiv_mem); the construction here takes an
arbitrary k-derivation, as Włodarczyk's argument does, because the stalk of the derivative
ideal sheaf at a non-closed point involves k-derivations that are not combinations of the ∂ᵢ
(Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean). Compare Kollár's computation of the
transformed derivatives in the chart, [Kol07, 75].
The derivation x_r · δ̃ of R[1/x_r], δ̃ the extension of δ by the quotient rule:
Włodarczyk's "any derivation D of 𝒪_X induces a derivation y σ^*(D) of 𝒪_{X'}" (the
proof of [Wlo05, Lemma 2.6.3]), before restriction to the chart ring.
Equations
- Derivation.awayBlowUpLift x r δ = (algebraMap R (Localization.Away (x r))) (x r) • Derivation.localization (Submonoid.powers (x r)) δ
Instances For
x_r · δ̃ agrees with x_r · δ on the image of R.
The table of derivatives of the proof of [Wlo05, Lemma 2.6.3], for an arbitrary derivation:
on the chart function yⱼ = xⱼ/x_r, x_r · δ̃(yⱼ) = δ(xⱼ) − yⱼ · δ(x_r) (Leibniz for
yⱼ · x_r = xⱼ).
x_r · δ̃ preserves the chart ring R' = R[yⱼ : j < r] — it sends the generators yⱼ and
the image of R into R', and R' is closed under sums and Leibniz products.
The derivation D' = y σ^*(D) of the chart ring R' induced by a k-derivation D = δ of
R (the proof of [Wlo05, Lemma 2.6.3]) — x_r · δ̃ restricted to R' ⊆ R[1/x_r].
Equations
- Derivation.blowupLift x r δ = (Derivation.awayBlowUpLift x r δ).restrictSubalgebra (IsLocalRing.chartRing x r) ⋯
Instances For
The defining identity of the lift: in R[1/x_r], D'(z) = x_r · δ̃(z).