Documentation

TauCeti.LinearAlgebra.SymmetricAlgebra.Derivation.OfEnd

Derivations of a symmetric algebra induced by endomorphisms #

A linear endomorphism f of a module M over a commutative ring R extends uniquely to a derivation of the symmetric algebra SymmetricAlgebra R M, sending each generator ι x to ι (f x). The assignment f ↦ (its derivation) is a homomorphism of Lie algebras from Module.End R M, with the commutator bracket, to the derivation Lie algebra of the symmetric algebra. It is natural with respect to symmetric-algebra maps, and each induced derivation preserves every homogeneous submodule. When an algebra map out of the symmetric algebra turns f into multiplication by a scalar c on generators, it turns the induced derivation into multiplication by n * c in degree n, a twisted form of Euler's identity.

Specialising f to the endomorphisms ⁅x, -⁆ of a Lie module gives the action of a Lie algebra on its symmetric algebra, including the adjoint action; see TauCeti.LinearAlgebra.SymmetricAlgebra.LieModule.

Main definitions and results #

source
noncomputable def SymmetricAlgebra.derivationOfEnd (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] :
Module.End R M →ₗ⁅R⁆ Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)

The derivation of SymmetricAlgebra R M induced by a linear endomorphism f of M: the unique derivation sending each generator ι x to ι (f x). The assignment is a homomorphism of Lie algebras from Module.End R M, with the commutator bracket, to the derivation Lie algebra.

Instances For
    source
    theorem SymmetricAlgebra.derivationOfEnd_apply (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) :
    (derivationOfEnd R M) f = mkDerivation (ι R M ∘ₗ f)

    The derivation induced by f is the derivation extending ι ∘ f.

    source
    @[simp]
    theorem SymmetricAlgebra.derivationOfEnd_ι (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (x : M) :
    ((derivationOfEnd R M) f) ((ι R M) x) = (ι R M) (f x)

    The derivation induced by f sends the generator ι x to ι (f x).

    source
    @[simp]
    theorem SymmetricAlgebra.iterate_derivationOfEnd_ι (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (n : ℕ) (x : M) :
    (⇑((derivationOfEnd R M) f))^[n] ((ι R M) x) = (ι R M) ((f ^ n) x)

    The iterates of the derivation induced by f act on generators by the powers of f.

    source
    theorem SymmetricAlgebra.map_apply_derivationOfEnd (R : Type u) {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (φ : M →ₗ[R] N) {f : Module.End R M} {g : Module.End R N} (h : φ ∘ₗ f = g ∘ₗ φ) (p : SymmetricAlgebra R M) :
    (map R φ) (((derivationOfEnd R M) f) p) = ((derivationOfEnd R N) g) ((map R φ) p)

    A symmetric-algebra map induced by a linear map intertwining two endomorphisms intertwines the induced derivations.

    source
    theorem SymmetricAlgebra.derivationOfEnd_mem_homogeneousSubmodule (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) :
    ((derivationOfEnd R M) f) p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n

    The derivation induced by a linear endomorphism preserves every homogeneous submodule.

    source
    theorem AlgHom.apply_derivationOfEnd_eq_mul_of_mem_homogeneousSubmodule {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {A : Type u_1} [CommSemiring A] [Algebra R A] (φ : SymmetricAlgebra R M →ₐ[R] A) {f : Module.End R M} {c : A} (h : ∀ (x : M), φ ((SymmetricAlgebra.ι R M) (f x)) = c * φ ((SymmetricAlgebra.ι R M) x)) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) :
    φ (((SymmetricAlgebra.derivationOfEnd R M) f) p) = ↑n * c * φ p

    Euler's identity, twisted by an endomorphism. If an algebra map φ turns f into multiplication by c on generators, φ (ι (f x)) = c * φ (ι x), then on a homogeneous element of degree n it turns the derivation induced by f into multiplication by n * c. For f = 1 and φ the identity this is Euler's identity D p = n • p for the Euler derivation D.