Derivations of symmetric algebras

A derivation of SymmetricAlgebra R M is determined by its values on the canonical generators. Conversely, every linear map from M to a module over its symmetric algebra extends uniquely to a derivation. This file packages the extension and the resulting linear equivalence.

The public interface follows Mathlib's analogous Polynomial.mkDerivation and MvPolynomial.mkDerivation APIs.

The construction uses the trivial square-zero extension. A prescribed value f x is paired with the generator SymmetricAlgebra.ι R M x; the universal property of the symmetric algebra extends this pair multiplicatively, and projection to the square-zero component gives the derivation.

Main definitions and results

• SymmetricAlgebra.mkDerivation: extend prescribed values on the canonical generators.
• SymmetricAlgebra.derivation_ext: symmetric-algebra derivations agree when they agree on the canonical generators.
• SymmetricAlgebra.mkDerivationEquiv: derivations are linearly equivalent to their restrictions to the canonical generators.

Roadmap

This supplies the derivation input for the PBW action on SymmetricAlgebra R L, toward the Poincare--Birkhoff--Witt target in Layer 3 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

@[instance_reducible]

def SymmetricAlgebra.commOppositeModule (S : Type u_1) (A : Type u_2) [CommSemiring S] [AddCommMonoid A] [Module S A] : Module Sᵐᵒᵖ A

The right-module structure induced by commutativity, used by the square-zero extension.

Equations

• SymmetricAlgebra.commOppositeModule S A = Module.compHom A (RingEquiv.toOpposite S).symm.toRingHom

theorem SymmetricAlgebra.commCentralScalar (S : Type u_1) (A : Type u_2) [CommSemiring S] [AddCommMonoid A] [Module S A] : IsCentralScalar S A

theorem SymmetricAlgebra.derivation_ext {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid A] [Module R A] [Module (SymmetricAlgebra R M) A] {D₁ D₂ : Derivation R (SymmetricAlgebra R M) A} (h : ∀ (x : M), D₁ ((ι R M) x) = D₂ ((ι R M) x)) : D₁ = D₂

Two derivations of a symmetric algebra are equal if they agree on the canonical generators.

theorem SymmetricAlgebra.derivation_ext_iff {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid A] [Module R A] [Module (SymmetricAlgebra R M) A] {D₁ D₂ : Derivation R (SymmetricAlgebra R M) A} : D₁ = D₂ ↔ ∀ (x : M), D₁ ((ι R M) x) = D₂ ((ι R M) x)

noncomputable def SymmetricAlgebra.mkDerivation {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid A] [Module R A] [Module (SymmetricAlgebra R M) A] [IsScalarTower R (SymmetricAlgebra R M) A] : (M →ₗ[R] A) →ₗ[R] Derivation R (SymmetricAlgebra R M) A

The derivation on SymmetricAlgebra R M taking the prescribed value f x on each canonical generator SymmetricAlgebra.ι R M x.

Equations

• SymmetricAlgebra.mkDerivation = { toFun := SymmetricAlgebra.mkDerivationAux✝, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricAlgebra.mkDerivation_ι {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid A] [Module R A] [Module (SymmetricAlgebra R M) A] [IsScalarTower R (SymmetricAlgebra R M) A] (f : M →ₗ[R] A) (x : M) : (mkDerivation f) ((ι R M) x) = f x

mkDerivation takes the prescribed value on a canonical symmetric-algebra generator.

noncomputable def SymmetricAlgebra.mkDerivationEquiv {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid A] [Module R A] [Module (SymmetricAlgebra R M) A] [IsScalarTower R (SymmetricAlgebra R M) A] : (M →ₗ[R] A) ≃ₗ[R] Derivation R (SymmetricAlgebra R M) A

Restriction to the canonical generators identifies derivations of a symmetric algebra with linear maps out of its generating module.

Equations

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

@[simp]

theorem SymmetricAlgebra.mkDerivationEquiv_apply {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid A] [Module R A] [Module (SymmetricAlgebra R M) A] [IsScalarTower R (SymmetricAlgebra R M) A] (f : M →ₗ[R] A) : mkDerivationEquiv f = mkDerivation f

@[simp]

theorem SymmetricAlgebra.mkDerivationEquiv_symm_apply {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid A] [Module R A] [Module (SymmetricAlgebra R M) A] [IsScalarTower R (SymmetricAlgebra R M) A] (D : Derivation R (SymmetricAlgebra R M) A) : mkDerivationEquiv.symm D = ↑D ∘ₗ ι R M