Derivations on the symmetric algebra

The universal property of SymmetricAlgebra R M for derivations: an R-linear map f : M → SymmetricAlgebra R M extends uniquely to a self-derivation D : SymmetricAlgebra R M → SymmetricAlgebra R M with D ∘ ι = f. Packaged as a linear equivalence SymmetricAlgebra.liftDerivation between R-linear maps and self-derivations.

Sibling of Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean's lift (which gives the algebra-hom universal property). This file fills the mathlib gap for the derivation universal property — candidate for upstream.

Main definitions

• SymmetricAlgebra.liftDerivation — the linear equivalence between M →ₗ[R] SymmetricAlgebra R M and Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M).

Main results

• SymmetricAlgebra.derivation_ext — derivation extensionality on the generators ι R M. Two self-derivations of SymmetricAlgebra R M are equal iff they agree on ι R M y for all y : M.
• SymmetricAlgebra.liftDerivation_ι — the forward direction: liftDerivation f (ι R M y) = f y.

Construction

The forward direction uses the dual-number trick (Cartan-Eilenberg): the trivial square-zero extension tsze (S(M)) (S(M)) = S(M) ⊕ S(M) ε (with ε² = 0) carries an algebra structure such that an algebra hom φ : S(M) → tsze (S(M)) (S(M)) of the form s ↦ (s, D s) corresponds exactly to a derivation D. We construct φ via SymmetricAlgebra.lift applied to y ↦ (ι R M y, f y), then extract D s := (φ s).snd.

Derivation extensionality on generators

theorem SymmetricAlgebra.derivation_ext {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {D₁ D₂ : Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)} (h : ∀ (y : M), D₁ ((ι R M) y) = D₂ ((ι R M) y)) : D₁ = D₂

A self-derivation of SymmetricAlgebra R M is determined by its values on the canonical generators ι R M y. The standard universal property of derivations on a free commutative algebra.

theorem SymmetricAlgebra.derivation_ext_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {D₁ D₂ : Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)} : D₁ = D₂ ↔ ∀ (y : M), D₁ ((ι R M) y) = D₂ ((ι R M) y)

Construction via the dual-number trick

The forward map liftDerivation : (M →ₗ[R] S(M)) → Derivation R (S(M)) (S(M)), extended to a linear equivalence below.

Linearity in the input map

The forward map f ↦ liftDerivationFun f is R-linear, packaged via derivation_ext.

The bundled LinearEquiv

noncomputable def SymmetricAlgebra.liftDerivation {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] : (M →ₗ[R] SymmetricAlgebra R M) ≃ₗ[R] Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)

The derivation universal property of SymmetricAlgebra R M: an R-linear map f : M → SymmetricAlgebra R M extends uniquely to a self-derivation D : SymmetricAlgebra R M → SymmetricAlgebra R M. The correspondence is an R-linear equivalence.

The forward direction is constructed via the dual-number trick (see file docstring). The inverse is restriction-to-ι: D ↦ D.toLinearMap ∘ ι R M.

Equations

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

@[simp]

theorem SymmetricAlgebra.liftDerivation_apply_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f : M →ₗ[R] SymmetricAlgebra R M) (s : SymmetricAlgebra R M) : (liftDerivation f) s = ((SymmetricAlgebra.liftDerivationAlgHom✝ f) s).snd

@[simp]

theorem SymmetricAlgebra.liftDerivation_apply_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f : M →ₗ[R] SymmetricAlgebra R M) (y : M) : (liftDerivation f) ((ι R M) y) = f y

@[simp]

theorem SymmetricAlgebra.liftDerivation_symm_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (D : Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) : liftDerivation.symm D = ↑D ∘ₗ ι R M