Coordinate derivations over the coefficient field

Kollár's derivations are k-derivations ("Der_X … a k-bilinear map", [Kol07, Definition 73]; Włodarczyk's Der_K(𝒪_X), [Wlo05, Definition 2.6.1]), while the coordinate structure RegularCoords of Hironaka/Algebra/Local/Coords.lean carries the ∂ᵢ as ℚ-derivations. The spanning condition SpansDerivations must be read over the coefficient field k of the ring at hand: SpansDerivations ℚ is strictly stronger and fails for ℝ⟦X⟧, ℂ⟦X⟧ and the stalks of smooth varieties over ℝ or ℂ (a nonzero ℚ-derivation of the coefficient field, applied coefficientwise, is a ℚ-derivation killing every xᵢ; not formalized).

This file provides the k-linear theory: IsLinearOver k (the ∂ᵢ kill algebraMap k R), SpansDerivations ℚ → SpansDerivations k, the spanning identity in transported coordinates over k, the commutation of the transported derivations and the change of coordinates over k, the maximal-contact coordinate over k, and the two properties for K⟦X⟧ (IsLinearOver K from pderiv_C, SpansDerivations K by uniqueness of Taylor coefficients through Krull's intersection theorem, Hironaka/Algebra/Local/Taylor.lean). The ℚ-forms transportPderiv_comm, changeCoordsOfSpans, exists_coords_x_zero_eq, exists_maximalContact of Hironaka/Algebra/Local/Coords.lean and MaximalContact.lean remain valid with the stronger hypothesis.

def IsLocalRing.derivationOver {R : Type u_1} [CommRing R] {k : Type u_2} [CommRing k] [Algebra k R] [Algebra ℚ R] (D : Derivation ℚ R R) (hD : ∀ (a : k), D ((algebraMap k R) a) = 0) : Derivation k R R

A ℚ-derivation of R killing the image of k is a k-derivation (∂ᵢ(af) = a ∂ᵢf by Leibniz).

Equations

• IsLocalRing.derivationOver D hD = { toFun := ⇑D, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[simp]

theorem IsLocalRing.derivationOver_apply {R : Type u_1} [CommRing R] {k : Type u_2} [CommRing k] [Algebra k R] [Algebra ℚ R] (D : Derivation ℚ R R) (hD : ∀ (a : k), D ((algebraMap k R) a) = 0) (f : R) : (derivationOver D hD) f = D f

def IsLocalRing.RegularCoords.IsLinearOver {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (k : Type u_2) [CommRing k] [Algebra k R] : Prop

The coordinate structure is k-linear if every ∂ᵢ kills the image of the coefficient field k (so that the ∂ᵢ are k-derivations, as in [Kol07, Definition 73]).

Equations

• c.IsLinearOver k = ∀ (i : Fin n) (a : k), (c.pderiv i) ((algebraMap k R) a) = 0

def IsLocalRing.RegularCoords.pderivOver {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (i : Fin n) : Derivation k R R

∂ᵢ as a k-derivation.

Equations

• c.pderivOver hk i = IsLocalRing.derivationOver (c.pderiv i) ⋯

@[simp]

theorem IsLocalRing.RegularCoords.pderivOver_apply {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (i : Fin n) (f : R) : (c.pderivOver hk i) f = (c.pderiv i) f

theorem IsLocalRing.RegularCoords.isLinearOver_sum_smul {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (r : Fin n → R) (a : k) : (∑ l : Fin n, r l • c.pderiv l) ((algebraMap k R) a) = 0

Every R-combination of the ∂ᵢ is again k-linear.

theorem IsLocalRing.RegularCoords.SpansDerivations.of_rat {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] [Algebra ℚ k] [IsScalarTower ℚ k R] (hs : c.SpansDerivations ℚ) : c.SpansDerivations k

SpansDerivations ℚ implies SpansDerivations k (a k-derivation is a ℚ-derivation). The converse fails for k = ℝ, ℂ (not formalized).

theorem IsLocalRing.RegularCoords.transportPderiv_isLinearOver {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (x' : Fin n → R) (j : Fin n) (a : k) : (c.transportPderiv x' j) ((algebraMap k R) a) = 0

The transported derivations are k-linear when the ∂ₗ are.

theorem IsLocalRing.RegularCoords.SpansDerivations.transport_over {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hs : c.SpansDerivations k) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (δ : Derivation k R R) (f : R) : δ f = ∑ j : Fin n, δ (x' j) * (c.transportPderiv x' j) f

The spanning identity in transported coordinates, δ f = ∑ⱼ δ(x'ⱼ) ∂'ⱼ f for every k-derivation δ (the argument of SpansDerivations.transport read over k; no linearity hypothesis is needed here).

noncomputable def IsLocalRing.RegularCoords.transportPderivOver {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (x' : Fin n → R) (j : Fin n) : Derivation k R R

The transported derivation as a k-derivation.

Equations

• c.transportPderivOver hk x' j = IsLocalRing.derivationOver (c.transportPderiv x' j) ⋯

theorem IsLocalRing.RegularCoords.transportPderiv_comm_over {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (i j : Fin n) (f : R) : (c.transportPderiv x' i) ((c.transportPderiv x' j) f) = (c.transportPderiv x' j) ((c.transportPderiv x' i) f)

Under IsLinearOver k and SpansDerivations k the transported derivations commute — their commutator is a k-derivation killing every x'ₗ, hence zero by the spanning identity over k (the k-linear form of transportPderiv_comm).

noncomputable def IsLocalRing.RegularCoords.changeCoordsOfLinearSpans {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : RegularCoords R n

The change of coordinates over k (no commutation hypothesis needed): the form of the change of coordinates used for the stalks of smooth varieties and the rings of analytic germs.

Equations

• c.changeCoordsOfLinearSpans hk hs x' hx' = c.changeCoords x' hx' ⋯

theorem IsLocalRing.RegularCoords.changeCoordsOfLinearSpans_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : (c.changeCoordsOfLinearSpans hk hs x' hx').x = x'

theorem IsLocalRing.RegularCoords.changeCoordsOfLinearSpans_pderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : (c.changeCoordsOfLinearSpans hk hs x' hx').pderiv = c.transportPderiv x'

theorem IsLocalRing.RegularCoords.changeCoordsOfLinearSpans_isLinearOver {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : (c.changeCoordsOfLinearSpans hk hs x' hx').IsLinearOver k

The transported structure is again k-linear.

theorem IsLocalRing.RegularCoords.changeCoordsOfLinearSpans_spansDerivations {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : (c.changeCoordsOfLinearSpans hk hs x' hx').SpansDerivations k

The transported structure again spans the k-derivations.

theorem IsLocalRing.RegularCoords.reindex_isLinearOver {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (σ : Equiv.Perm (Fin n)) : (c.reindex σ).IsLinearOver k

theorem IsLocalRing.RegularCoords.reindex_spansDerivations {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hs : c.SpansDerivations k) (σ : Equiv.Perm (Fin n)) : (c.reindex σ).SpansDerivations k

theorem IsLocalRing.RegularCoords.exists_coords_x_zero_eq_over {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) {h : R} (hh : ordElem h = 1) : ∃ (hn : 0 < n) (c' : RegularCoords R n), c'.x ⟨0, hn⟩ = h ∧ (c'.pderiv ⟨0, hn⟩) h = 1 ∧ c'.IsLinearOver k ∧ c'.SpansDerivations k

Under IsLinearOver k and SpansDerivations k, an element of order 1 is the first coordinate of a k-linear, k-spanning coordinate system x' with ∂'₁ h = 1 (the coordinate half of the local construction of maximal contact, [Kol07, 51.2], over k).

theorem IsLocalRing.RegularCoords.exists_maximalContact_over {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {k : Type u_2} [CommRing k] [Algebra k R] (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) {I : Ideal R} {m : ℕ} (hm : 1 ≤ m) (hI : ord I = ↑m) : ∃ h ∈ c.MC I m, ordElem h = 1 ∧ ∃ (hn : 0 < n) (c' : RegularCoords R n), c'.x ⟨0, hn⟩ = h ∧ (c'.pderiv ⟨0, hn⟩) h = 1

The local construction of maximal contact [Kol07, 51.2] over k: for ord I = m ≥ 1 some h ∈ MC_m(I) of order 1 is the first coordinate of a coordinate system x' with ∂'₁ h = 1.

The two properties for K⟦X⟧

theorem IsLocalRing.derivation_mem_maximalIdeal_pow {K : Type u_2} [Field K] {n : ℕ} (δ : Derivation K (MvPowerSeries (Fin n) K) (MvPowerSeries (Fin n) K)) (N : ℕ) {f : MvPowerSeries (Fin n) K} (hf : f ∈ maximalIdeal (MvPowerSeries (Fin n) K) ^ (N + 1)) : δ f ∈ maximalIdeal (MvPowerSeries (Fin n) K) ^ N

A K-derivation of K⟦X⟧ lowers the 𝔪-adic order by at most one (Leibniz on a product of elements of 𝔪).

theorem IsLocalRing.derivation_coe_eq_sum {K : Type u_2} [Field K] {n : ℕ} (δ : Derivation K (MvPowerSeries (Fin n) K) (MvPowerSeries (Fin n) K)) (P : MvPolynomial (Fin n) K) : δ ↑P = ∑ i : Fin n, δ (MvPowerSeries.X i) * (MvPowerSeries.pderiv i) ↑P

A K-derivation of K⟦X⟧ agrees with ∑ᵢ δ(Xᵢ) ∂ᵢ on polynomials (Leibniz).

theorem IsLocalRing.mvPowerSeries_isLinearOver (K : Type u_2) [Field K] (n : ℕ) [CharZero K] : (RegularCoords.stdMvPowerSeries K n).IsLinearOver K

The coordinate structure RegularCoords.mvPowerSeries on K⟦X⟧ is K-linear (MvPowerSeries.pderiv_C).

theorem IsLocalRing.mvPowerSeries_spansDerivations (K : Type u_2) [Field K] (n : ℕ) [CharZero K] : (RegularCoords.stdMvPowerSeries K n).SpansDerivations K

The coordinate structure on K⟦X⟧ spans the K-derivations — a K-derivation agrees with ∑ᵢ δ(Xᵢ) ∂ᵢ on polynomials, both sides lower the 𝔪-adic order by at most one, and Krull's intersection theorem (Hironaka/Algebra/Local/Taylor.lean) finishes: the uniqueness of Taylor coefficients.