Documentation

Mathlib.Algebra.Lie.Derivation.BaseChange

LieDerivations of a Lie algebra created through BaseChange #

When, given an R-algebra A and an R-Lie algebra L the (Lie algebra) basechange A ⊗[R] L, both derivations of A and Lie derivations of L induce Lie derivations of A ⊗[R] L. Moreover, both these procedures are Lie algebra homomorphisms themselves.

Tags #

lie algebra, extension of scalars, base change, derivation

source
def Lie.Derivation.ofDerivation {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] (L : Type u_3) [LieRing L] [LieAlgebra R L] :
Derivation R A A →ₗ⁅R⁆ LieDerivation R (TensorProduct R A L) (TensorProduct R A L)

A derivation of an associative R-algebra A, induces a Lie derivation of A ⊗[R] L for any Lie algebra L over R.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Lie.Derivation.ofDerivation_apply {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {L : Type u_3} [LieRing L] [LieAlgebra R L] (d : Derivation R A A) (x : TensorProduct R A L) :
    ((ofDerivation L) d) x = (LinearMap.rTensor L ↑d) x
    source
    def Lie.Derivation.ofLieDerivation {R : Type u_1} [CommRing R] (A : Type u_2) [CommRing A] [Algebra R A] {L : Type u_3} [LieRing L] [LieAlgebra R L] :
    LieDerivation R L L →ₗ⁅R⁆ LieDerivation R (TensorProduct R A L) (TensorProduct R A L)

    A Lie derivation of an R-Lie algebra L, induces a Lie derivation of A ⊗[R] L for any Algebra A over R.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Lie.Derivation.ofLieDerivation_apply {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {L : Type u_3} [LieRing L] [LieAlgebra R L] (d : LieDerivation R L L) (x : TensorProduct R A L) :
      ((ofLieDerivation A) d) x = (LinearMap.lTensor A ↑d) x