The chart ring: injectivity, the transformed derivations, the presentation, the origin #
R is a regular local ring, x : Fin n → R a regular system of parameters, r : Fin n, and
R' = R[xᵢ/x_r : i < r] ⊆ R[1/x_r] the chart ring of Hironaka/Algebra/Local/ChartRing.lean: the
ring of Kollár's chart (60.2) of the blow-up of (x₁ = ⋯ = x_r = 0) [Kol07, Definition 60]. This
file proves its basic properties: the injectivity of R → R', the extension of derivations to
R[1/a], the identities ∂'ⱼ yₖ = δⱼₖ for the transformed derivations and the stability of
R' under them, the surjectivity of the presentation R[Y_i : i < r] → R', and the origin 𝔪'
of the chart together with the other rational points 𝔪'_a of the exceptional fibre (maximal
ideals lying over 𝔪 with the same residue field).
The algebra map is injective #
R is a domain (isDomain_of_isRegularLocalRing) and x_r ≠ 0 (it is not even in 𝔪²), so
R → R[1/x_r] is injective (IsLocalization.injective), and R → R' is its restriction.
Extension of derivations #
D.extendAway a is Derivation.localization at Submonoid.powers a; it restricts to D, it
is the unique such derivation, and on f/aᵐ it is given by the quotient rule
(a · D f − m · f · D a)/aᵐ⁺¹: the general formula (s · D f − f · D s)/s² with s = aᵐ and
D(aᵐ) = m aᵐ⁻¹ D a, cleared of the common factor aᵐ⁻¹.
The transformed derivations #
Write u = 1/x_r ∈ R[1/x_r], so x_r u = 1, yₖ = xₖ u for k < r and yₖ = xₖ for k ≥ r.
Each extended coordinate derivation ∂ⱼ satisfies ∂ⱼ u = −u² ∂ⱼ(x_r) = −δⱼᵣ u²
(Derivation.leibniz_of_mul_eq_one), hence, by Leibniz, ∂ⱼ yₖ = δⱼₖ u − δⱼᵣ xₖ u² for k < r
and ∂ⱼ yₖ = δⱼₖ for k ≥ r. The transformed derivations ∂'ⱼ = x_r ∂ⱼ (j < r),
∂'_r = ∂_r + ∑_{i<r} yᵢ ∂ᵢ, ∂'ⱼ = ∂ⱼ (j > r) then give ∂'ⱼ yₖ = δⱼₖ by the identity
x_r u = 1: for j < r the factor x_r cancels the u; for j = r and k < r the term
−xₖ u² of ∂_r yₖ is cancelled by the single surviving term yₖ ∂ₖ yₖ = xₖ u · u of the sum
(the table of derivatives in the proof of [Wlo05, Lemma 2.6.3]; [BM08, Lemma 3.1]). Each ∂'ⱼ
maps R' into R'
because it maps the generators yₖ (k < r) and the image of R into R' (∂'ⱼ(a) = x_r ∂ⱼ a,
∂_r a + ∑ yᵢ ∂ᵢ a or ∂ⱼ a) and R' is closed under sums and Leibniz products
(Algebra.adjoin_induction).
The presentation is surjective #
R[Y_i : i < r] → R' has range Algebra.adjoin R {yᵢ : i < r} (MvPolynomial.aeval_range),
which is all of R' by definition of the chart ring. The kernel (the Koszul relations) is
computed in Hironaka/Algebra/Local/ChartPresentation.lean.
The origin and the other points of the fibre #
𝔪' = ⟨y₁, …, yₙ⟩ R' is a maximal ideal lying over 𝔪 with residue field K: Kollár's "p',
the origin of the chart" in the proof of [Kol07, Lemma 61]. The shifted coordinates
x'ᵢ = xᵢ − ãᵢ x_r define the same chart ring with the point 𝔪'_a as origin: Kollár's linear
change of the (x₁, …, x_r)-coordinates that "moves the origin of the chart" in the same
proof. The transformed derivations, packaged as derivations of R' (chartDerivRing), are the
coordinate derivations of the chart used in Hironaka/Algebra/Local/ChartCoords.lean and
Hironaka/Algebra/Local/TransformDeriv.lean.
A finite sum of derivations, applied.
D.extendAway a restricts to D.
Uniqueness of the extension.
The quotient rule D(f/aᵐ) = (a · D f − m · f · D a)/aᵐ⁺¹.
A member of a regular system of parameters is nonzero (it is not even in 𝔪²).
R → R[1/x_r] is injective.
The algebra map R → R' into the chart ring is injective.
u = 1/x_r in R[1/x_r].
Equations
- IsLocalRing.invX x r = Localization.mk 1 ⟨x r, ⋯⟩
Instances For
The table of derivatives of the chart coordinates (the proof of [Wlo05, Lemma 2.6.3]):
∂ⱼ yₖ = δⱼₖ u − δⱼᵣ xₖ u² for k < r.
∂'ⱼ yₖ = δⱼₖ: the transformed derivations are dual to the chart coordinates (the proof of
[Wlo05, Lemma 2.6.3]; [BM08, Lemma 3.1]).
∂'ⱼ maps the image of R into the chart ring.
Each ∂'ⱼ maps the chart ring R' into itself.
Every element of the chart ring is congruent modulo 𝔪' to the image of an element of R
(the constant term of a polynomial in the yᵢ).
The key point, 1 ∉ 𝔪': the origin of the chart in the proof of [Kol07, Lemma 61] is a
point. Proof: R/⟨xᵢ : i ≠ r⟩ is a regular local ring of dimension one
(Hironaka/Algebra/Local/RegularSystem.lean, after moving x_r to the last position) with maximal
ideal ⟨x̄_r⟩, hence a domain in which x̄_r ≠ 0; the ring map from R[1/x_r] to its fraction
field sends R' into the quotient and every generator of 𝔪' into its maximal ideal, so 1 ∈ 𝔪'
would give 1 ∈ ⟨x̄_r⟩.
1 ∉ 𝔪'.
𝔪' is a proper ideal.
𝔪' lies over 𝔪 (general denominator).
𝔪' lies over 𝔪.
R'/𝔪' ≅ K, as the bijectivity of the residue map R/𝔪 → R'/𝔪'.
The origin of the chart is a maximal ideal of R' (the point p' of the proof of
[Kol07, Lemma 61]).
x'ᵢ/x_r = yᵢ − ãᵢ for i < r.
The shifted coordinates generate 𝔪 (the linear change of coordinates in the proof of
[Kol07, Lemma 61]).
1 ∉ 𝔪'_a.
𝔪'_a lies over 𝔪.
𝔪'_a has residue field K: 𝔪 maps into 𝔪'_a and the residue map is bijective.
𝔪'_a is maximal.
R[1/x_r] is a domain.
The chart ring is a domain.
∂'ⱼ as a derivation of the chart ring R' (it preserves R' by chartDeriv_mem): the
coordinate derivations of the chart, used in Hironaka/Algebra/Local/ChartCoords.lean and
Hironaka/Algebra/Local/TransformDeriv.lean.
Equations
- c.chartDerivRing r j = { toFun := fun (z : ↥(IsLocalRing.chartRing c.x r)) => ⟨(c.chartDeriv r j) ↑z, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
Instances For
A permutation of Fin n carrying the initial segment of length s.card onto s, with the last
element of the segment going to a prescribed k ∈ s (Kollár's convention Z = (y_1 = ⋯ = y_r = 0)
with the chart coordinate y_r); a combinatorial tool for the charts of
Hironaka/Resolution/Algebraic/Monomial/Geometric/Chart.lean.