Derivations of the chart ring dual to the chart functions

On the chart ring R' = R[x_i/x_r : i < r] ⊆ R[1/x_r] of the blow-up of R along (x_0, …, x_r) [Kol07, Definition 60], the chart functions are y_i = x_i/x_r (i < r), y_r = x_r, and y_m = x_m (m > r). Given derivations D_i of R over k dual to the regular system of parameters x (D_i x_j = δ_{ij}, supplied at a stalk by Hironaka.Scheme.Snc.StalkDerivations), the chart ring carries derivations dual to the chart functions (chartRingDer, chartRingDer_chartYR):

• D_m for m > r extends to R[1/x_r] (the quotient rule) and kills every y_i = x_i/x_r, i < r, since it kills x_i and x_r;
• x_r · D_i for i < r sends y_j to δ_{ij} — from y_j x_r = x_j and the Leibniz rule, x_r D_i(y_j) = D_i(x_j) − y_j D_i(x_r) = δ_{ij} — and x_m (m ≥ r) to 0;
• E = D_r + ∑_{l < r} y_l D_l sends y_j to 0 (x_r E(y_j) = −y_j + y_j = 0), x_r to 1 and x_m (m > r) to 0.

Each of these preserves the subalgebra R' (checked on the generators y_i and the constants, then by the Leibniz rule along Algebra.adjoin_induction), so restricts to R' (Derivation.restrictSubalgebra), and localizes to R'_𝔮 at any prime 𝔮. Consequently the chart functions lying in the maximal ideal of a regular localization R'_𝔮 have linearly independent classes in the cotangent space and extend to a regular system of parameters (exists_span_eq_maximalIdeal_extend_chartYR; the argument of Hironaka.Scheme.Snc.EtaleParameters). This is the coordinate content of Hau14, Proposition 5.4 (6) and [Hau03, Appendix C (7)] at an arbitrary point of the chart.

noncomputable def Derivation.restrictSubalgebra {k : Type u_1} {R : Type u_2} {L : Type u_3} [CommRing k] [CommRing R] [CommRing L] [Algebra k R] [Algebra R L] [Algebra k L] [IsScalarTower k R L] (D : Derivation k L L) (S : Subalgebra R L) (hS : ∀ a ∈ S, D a ∈ S) : Derivation k ↥S ↥S

A derivation of L over k preserving an R-subalgebra S restricts to a derivation of S.

Equations

• D.restrictSubalgebra S hS = { toFun := fun (a : ↥S) => ⟨D ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

theorem Derivation.coe_restrictSubalgebra_apply {k : Type u_1} {R : Type u_2} {L : Type u_3} [CommRing k] [CommRing R] [CommRing L] [Algebra k R] [Algebra R L] [Algebra k L] [IsScalarTower k R L] (D : Derivation k L L) (S : Subalgebra R L) (hS : ∀ a ∈ S, D a ∈ S) (a : ↥S) : ↑((D.restrictSubalgebra S hS) a) = D ↑a

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.awayDer {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (i : Fin n) : Derivation k (Localization.Away (x r)) (Localization.Away (x r))

The extension of D_i to R[1/x_r] (the quotient rule).

Equations

• AlgebraicGeometry.awayDer x r D i = Derivation.localization (Submonoid.powers (x r)) (D i)

theorem AlgebraicGeometry.awayDer_algebraMap {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (i : Fin n) (a : R) : (awayDer x r D i) ((algebraMap R (Localization.Away (x r))) a) = (algebraMap R (Localization.Away (x r))) ((D i) a)

theorem AlgebraicGeometry.chartY_mul_algebraMap {R : Type u_2} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {j : Fin n} (hj : j < r) : IsLocalRing.chartY x r j * (algebraMap R (Localization.Away (x r))) (x r) = (algebraMap R (Localization.Away (x r))) (x j)

y_j · x_r = x_j in R[1/x_r] for j < r.

theorem AlgebraicGeometry.isUnit_algebraMap_self {R : Type u_2} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : IsUnit ((algebraMap R (Localization.Away (x r))) (x r))

theorem AlgebraicGeometry.awayDer_chartY_mul {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (i : Fin n) {j : Fin n} (hj : j < r) : (awayDer x r D i) (IsLocalRing.chartY x r j) * (algebraMap R (Localization.Away (x r))) (x r) = (algebraMap R (Localization.Away (x r))) ((D i) (x j)) - IsLocalRing.chartY x r j * (algebraMap R (Localization.Away (x r))) ((D i) (x r))

The Leibniz relation for the chart function y_j = x_j / x_r: x_r · D(y_j) = D(x_j) − y_j · D(x_r).

noncomputable def AlgebraicGeometry.chartDer {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (i : Fin n) : Derivation k (Localization.Away (x r)) (Localization.Away (x r))

The derivations of R[1/x_r] dual to the chart functions: x_r · D_i for the fibre coordinates i < r, D_r + ∑_{l < r} y_l D_l for x_r, and D_m for m > r.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.chartDer_of_lt {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) {i : Fin n} (hi : i < r) : chartDer x r D i = (algebraMap R (Localization.Away (x r))) (x r) • awayDer x r D i

theorem AlgebraicGeometry.chartDer_self {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) : chartDer x r D r = awayDer x r D r + ∑ l : Fin n with l < r, IsLocalRing.chartY x r l • awayDer x r D l

theorem AlgebraicGeometry.chartDer_of_gt {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) {i : Fin n} (hi : ¬i < r) (hir : i ≠ r) : chartDer x r D i = awayDer x r D i

theorem AlgebraicGeometry.chartDer_chartY {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (hD : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (i j : Fin n) : (chartDer x r D i) (IsLocalRing.chartY x r j) = if i = j then 1 else 0

The chart derivations are dual to the chart functions: chartDer i (y_j) = δ_{ij}.

theorem AlgebraicGeometry.chartDer_mem {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (hD : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (i : Fin n) (a : Localization.Away (x r)) : a ∈ IsLocalRing.chartRing x r → (chartDer x r D i) a ∈ IsLocalRing.chartRing x r

The chart derivations preserve the chart ring R' = R[y_i : i < r].

noncomputable def AlgebraicGeometry.chartRingDer {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (hD : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (i : Fin n) : Derivation k ↥(IsLocalRing.chartRing x r) ↥(IsLocalRing.chartRing x r)

The derivations of the chart ring dual to the chart functions y_i ∈ R'.

Equations

• AlgebraicGeometry.chartRingDer x r D hD i = (AlgebraicGeometry.chartDer x r D i).restrictSubalgebra (IsLocalRing.chartRing x r) ⋯

theorem AlgebraicGeometry.chartRingDer_chartYR {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (hD : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (i j : Fin n) : (chartRingDer x r D hD i) (IsLocalRing.chartYR x r j) = if i = j then 1 else 0

theorem AlgebraicGeometry.exists_span_eq_maximalIdeal_extend_chartYR {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (r : Fin n) (D : Fin n → Derivation k R R) (hD : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (𝔮 : Ideal ↥(IsLocalRing.chartRing x r)) [𝔮.IsPrime] [IsRegularLocalRing (Localization.AtPrime 𝔮)] : ∃ (m : ℕ) (z' : Fin m → Localization.AtPrime 𝔮), (Ideal.span (Set.range z') = IsLocalRing.maximalIdeal (Localization.AtPrime 𝔮) ∧ ↑m = ringKrullDim (Localization.AtPrime 𝔮)) ∧ ∃ (σ : { i : Fin n // (algebraMap (↥(IsLocalRing.chartRing x r)) (Localization.AtPrime 𝔮)) (IsLocalRing.chartYR x r i) ∈ IsLocalRing.maximalIdeal (Localization.AtPrime 𝔮) } → Fin m), Function.Injective σ ∧ ∀ (i : { i : Fin n // (algebraMap (↥(IsLocalRing.chartRing x r)) (Localization.AtPrime 𝔮)) (IsLocalRing.chartYR x r i) ∈ IsLocalRing.maximalIdeal (Localization.AtPrime 𝔮) }), z' (σ i) = (algebraMap (↥(IsLocalRing.chartRing x r)) (Localization.AtPrime 𝔮)) (IsLocalRing.chartYR x r ↑i)

The coordinate content of [Hau14, Proposition 5.4 (6)] on the chart ring: at a prime 𝔮 of the chart ring with R'_𝔮 regular, the chart functions lying in the maximal ideal of R'_𝔮 extend to a regular system of parameters.