Extending a derivation to a localization

A derivation D : A → A over k extends to the localization M⁻¹A by the quotient rule D (a / s) = (s · D a - a · D s) / s², and the extension is the unique derivation of M⁻¹A compatible with D on A. The sources use this silently: Włodarczyk notes that the derivations ∂/∂uᵢ of a local ring extend to the field of rational functions [Wlo05, Lemma 2.6.3, proof], and Kollár's chart formulas for the transform of a marked ideal [Kol07, Definition 60] are computations in the localization at the exceptional coordinate xᵣ. Mathlib has no such extension, so it is built here for an arbitrary submonoid M; the localization away from one element r is the case M = Submonoid.powers r.

Main declarations

• Derivation.localization M D : Derivation k (Localization M) (Localization M), with Derivation.localizationFun_mk giving its value on Localization.mk a s.
• Derivation.localization_algebraMap: compatibility with D on the image of A.
• Derivation.eq_localization_of_algebraMap: uniqueness.
• Derivation.localization_comm: the extensions of commuting derivations commute.

Proof

Well-definedness on fractions is the only computation: if u (t a) = u (s c) for some u ∈ M, then applying D and multiplying out shows u² t² (s D a - a D s) = u² s² (t D c - c D t), so the two candidate values agree in M⁻¹A. Additivity, k-linearity and the Leibniz rule are polynomial identities checked after clearing denominators. Uniqueness: a derivation of M⁻¹A agreeing with D on A is determined on 1/s by D'(1/s) = -(1/s)² D'(s) (Derivation.leibniz_of_mul_eq_one) and hence on every a/s.

noncomputable def Derivation.localizationFun {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) (D : Derivation k A A) (x : Localization M) : Localization M

The value of the extended derivation on the fraction a / s: (s · D a - a · D s) / s², the quotient rule.

Equations

• Derivation.localizationFun M D x = x.liftOn (fun (a : A) (s : ↥M) => Localization.mk (↑s * D a - a * D ↑s) (s * s)) ⋯

@[simp]

theorem Derivation.localizationFun_mk {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) (D : Derivation k A A) (a : A) (s : ↥M) : localizationFun M D (Localization.mk a s) = Localization.mk (↑s * D a - a * D ↑s) (s * s)

noncomputable def Derivation.localization {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) (D : Derivation k A A) : Derivation k (Localization M) (Localization M)

Extension of a derivation to a localization: the derivation a / s ↦ (s · D a - a · D s) / s² of M⁻¹A. Not stated in the sources, which use it silently [Wlo05, Lemma 2.6.3, proof].

Equations

• Derivation.localization M D = { toFun := Derivation.localizationFun M D, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[simp]

theorem Derivation.localization_mk {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) (D : Derivation k A A) (a : A) (s : ↥M) : (localization M D) (Localization.mk a s) = Localization.mk (↑s * D a - a * D ↑s) (s * s)

@[simp]

theorem Derivation.localization_algebraMap {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) (D : Derivation k A A) (a : A) : (localization M D) ((algebraMap A (Localization M)) a) = (algebraMap A (Localization M)) (D a)

The extension agrees with D on the image of A.

theorem Derivation.eq_localization_of_algebraMap {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) (D : Derivation k A A) (D' : Derivation k (Localization M) (Localization M)) (h : ∀ (a : A), D' ((algebraMap A (Localization M)) a) = (algebraMap A (Localization M)) (D a)) : D' = localization M D

Uniqueness: a derivation of M⁻¹A that agrees with D on A is the extension.

theorem Derivation.zero_localization {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) : localization M 0 = 0

The extension of the zero derivation is zero.

theorem Derivation.localization_comm {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (M : Submonoid A) (D₁ D₂ : Derivation k A A) (h : ∀ (a : A), D₁ (D₂ a) = D₂ (D₁ a)) (z : Localization M) : (localization M D₁) ((localization M D₂) z) = (localization M D₂) ((localization M D₁) z)

The extensions of two commuting derivations commute: their commutator is a derivation of M⁻¹A vanishing on A, hence zero by uniqueness.