Derivations of a localization

Let T be a localization of a commutative ring A at a submonoid S, and let N be a T-module. Every R-derivation A → N extends uniquely to an R-derivation T → N, by the quotient rule D (a / s) = (s • D a - a • D s) / s ^ 2.

Uniqueness is elementary: if t * s = a in T with s ∈ S, the Leibniz rule gives s • D t = D a - t • D s, and s acts invertibly on N. The uniqueness statement only needs commutative semirings, left cancellative addition in N, and a multiplicative action of T. Existence goes through Kähler differentials: Ω[T⁄R] is the localization of Ω[A⁄R] at S (KaehlerDifferential.isLocalizedModule_map), so the A-linear map Ω[A⁄R] → N classifying a derivation of A extends to a T-linear map Ω[T⁄R] → N.

These are the algebraic inputs for computing the sheaf of relative differentials of an affine scheme on its basic open subsets.

Main declarations

• IsLocalization.eq_of_leibniz: two maps T → N satisfying the Leibniz rule and agreeing on the image of A are equal;
• Derivation.extendOfIsLocalization: the extension of a derivation of A to T, with Derivation.extendOfIsLocalization_algebraMap stating that it extends.

theorem IsLocalization.eq_of_leibniz {A : Type u_1} {T : Type u_2} {N : Type u_3} [CommSemiring A] [CommSemiring T] [Algebra A T] [Add N] [IsLeftCancelAdd N] [MulAction T N] (S : Submonoid A) [IsLocalization S T] {δ₁ δ₂ : T → N} (h₁ : ∀ (x y : T), δ₁ (x * y) = x • δ₁ y + y • δ₁ x) (h₂ : ∀ (x y : T), δ₂ (x * y) = x • δ₂ y + y • δ₂ x) (h : ∀ (a : A), δ₁ ((algebraMap A T) a) = δ₂ ((algebraMap A T) a)) : δ₁ = δ₂

Two maps from a localization T of a commutative semiring A to a type with left cancellative addition and a multiplicative T-action that satisfy the Leibniz rule are equal once they agree on the image of A. In particular a derivation of T is determined by its values on A.

noncomputable def Derivation.extendOfIsLocalization {R : Type u_1} {A : Type u_2} {T : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [CommRing T] [Algebra R T] [Algebra A T] [AddCommGroup N] [Module T N] [Module R N] [Algebra R A] [IsScalarTower R A T] [Module A N] [IsScalarTower A T N] [IsScalarTower R A N] (S : Submonoid A) [IsLocalization S T] (D : Derivation R A N) : Derivation R T N

The extension of an R-derivation D : A → N to an R-derivation of the localization T of A at S, for N a T-module. By IsLocalization.eq_of_leibniz it is the only derivation of T agreeing with D on A.

Equations

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

@[simp]

theorem Derivation.extendOfIsLocalization_algebraMap {R : Type u_1} {A : Type u_2} {T : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [CommRing T] [Algebra R T] [Algebra A T] [AddCommGroup N] [Module T N] [Module R N] [Algebra R A] [IsScalarTower R A T] [Module A N] [IsScalarTower A T N] [IsScalarTower R A N] (S : Submonoid A) [IsLocalization S T] (D : Derivation R A N) (a : A) : (extendOfIsLocalization S D) ((algebraMap A T) a) = D a

The extension of D to the localization T agrees with D on the image of A.