Lie derivations

This file defines Lie derivations and establishes some basic properties.

Main definitions

• LieDerivation: A Lie derivation D from the Lie R-algebra L to the L-module M is an R-linear map that satisfies the Leibniz rule D [a, b] = [a, D b] - [b, D a].
• LieDerivation.inner: The natural map from a Lie module to the derivations taking values in it.

Main statements

• LieDerivation.eqOn_lieSpan: two Lie derivations equal on a set are equal on its Lie span.
• LieDerivation.instLieAlgebra: the set of Lie derivations from a Lie algebra to itself is a Lie algebra.

Implementation notes

• Mathematically, a Lie derivation is just a derivation on a Lie algebra. However, the current implementation of RingTheory.Derivation requires a commutative associative algebra, so is incompatible with the setting of Lie algebras. Initially, this file is a copy-pasted adaptation of the RingTheory.Derivation.Basic.lean file.
• Since we don't have right actions of Lie algebras, the second term in the Leibniz rule is written as - [b, D a]. Within Lie algebras, skew symmetry restores the expected definition [D a, b].

structure LieDerivation (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] extends L →ₗ[R] M : Type (max u_2 u_3)

A Lie derivation D from the Lie R-algebra L to the L-module M is an R-linear map that satisfies the Leibniz rule D [a, b] = [a, D b] - [b, D a].

• toFun : L → M
• map_add' (x y : L) : (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
• map_smul' (m : R) (x : L) : (↑self).toFun (m • x) = (RingHom.id R) m • (↑self).toFun x
• leibniz' (a b : L) : ↑self ⁅a, b⁆ = ⁅a, ↑self b⁆ - ⁅b, ↑self a⁆

instance LieDerivation.instFunLike {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : FunLike (LieDerivation R L M) L M

Equations

• LieDerivation.instFunLike = { coe := fun (D : LieDerivation R L M) => (↑D).toFun, coe_injective' := ⋯ }

instance LieDerivation.instLinearMapClass {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LinearMapClass (LieDerivation R L M) R L M

theorem LieDerivation.toFun_eq_coe {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) : (↑D).toFun = ⇑D

def LieDerivation.Simps.apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) : L → M

See Note [custom simps projection]

Equations

• LieDerivation.Simps.apply D = ⇑D

instance LieDerivation.instCoeToLinearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Coe (LieDerivation R L M) (L →ₗ[R] M)

Equations

• LieDerivation.instCoeToLinearMap = { coe := fun (D : LieDerivation R L M) => ↑D }

@[simp]

theorem LieDerivation.mk_coe {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : L →ₗ[R] M) (h₁ : ∀ (a b : L), f ⁅a, b⁆ = ⁅a, f b⁆ - ⁅b, f a⁆) : ⇑{ toLinearMap := f, leibniz' := h₁ } = ⇑f

@[simp]

theorem LieDerivation.coeFn_coe {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : LieDerivation R L M) : ⇑↑f = ⇑f

theorem LieDerivation.coe_injective {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Function.Injective DFunLike.coe

theorem LieDerivation.ext {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} (H : ∀ (a : L), D1 a = D2 a) : D1 = D2

theorem LieDerivation.ext_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} : D1 = D2 ↔ ∀ (a : L), D1 a = D2 a

theorem LieDerivation.congr_fun {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} (h : D1 = D2) (a : L) : D1 a = D2 a

@[simp]

theorem LieDerivation.apply_lie_eq_sub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a b : L) : D ⁅a, b⁆ = ⁅a, D b⁆ - ⁅b, D a⁆

theorem LieDerivation.apply_lie_eq_add {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (a b : L) : D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆

For a Lie derivation from a Lie algebra to itself, the usual Leibniz rule holds.

theorem LieDerivation.eqOn_lieSpan {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} {s : Set L} (h : Set.EqOn (⇑D1) (⇑D2) s) : Set.EqOn ⇑D1 ⇑D2 ↑(LieSubalgebra.lieSpan R L s)

Two Lie derivations equal on a set are equal on its Lie span.

theorem LieDerivation.ext_of_lieSpan_eq_top {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} (s : Set L) (hs : LieSubalgebra.lieSpan R L s = ⊤) (h : Set.EqOn (⇑D1) (⇑D2) s) : D1 = D2

If the Lie span of a set is the whole Lie algebra, then two Lie derivations equal on this set are equal on the whole Lie algebra.

theorem LieDerivation.iterate_apply_lie {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (n : ℕ) (a b : L) : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆

The general Leibniz rule for Lie derivatives.

theorem LieDerivation.iterate_apply_lie' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (n : ℕ) (a b : L) : (⇑D)^[n] ⁅a, b⁆ = ∑ i ∈ Finset.range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆

Alternate version of the general Leibniz rule for Lie derivatives.

instance LieDerivation.instZero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Zero (LieDerivation R L M)

Equations

• LieDerivation.instZero = { zero := let __LinearMap := 0; { toLinearMap := __LinearMap, leibniz' := ⋯ } }

@[simp]

theorem LieDerivation.coe_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : ⇑0 = 0

@[simp]

theorem LieDerivation.coe_zero_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : ↑0 = 0

theorem LieDerivation.zero_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (a : L) : 0 a = 0

instance LieDerivation.instInhabited {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Inhabited (LieDerivation R L M)

Equations

• LieDerivation.instInhabited = { default := 0 }

instance LieDerivation.instAdd {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Add (LieDerivation R L M)

Equations

• LieDerivation.instAdd = { add := fun (D1 D2 : LieDerivation R L M) => let __LinearMap := ↑D1 + ↑D2; { toLinearMap := __LinearMap, leibniz' := ⋯ } }

@[simp]

theorem LieDerivation.coe_add {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 D2 : LieDerivation R L M) : ⇑(D1 + D2) = ⇑D1 + ⇑D2

@[simp]

theorem LieDerivation.coe_add_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 D2 : LieDerivation R L M) : ↑(D1 + D2) = ↑D1 + ↑D2

theorem LieDerivation.add_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} (a : L) : (D1 + D2) a = D1 a + D2 a

theorem LieDerivation.map_neg {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a : L) : D (-a) = -D a

theorem LieDerivation.map_sub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a b : L) : D (a - b) = D a - D b

instance LieDerivation.instNeg {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Neg (LieDerivation R L M)

Equations

• LieDerivation.instNeg = { neg := fun (D : LieDerivation R L M) => { toLinearMap := -↑D, leibniz' := ⋯ } }

@[simp]

theorem LieDerivation.coe_neg {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) : ⇑(-D) = -⇑D

@[simp]

theorem LieDerivation.coe_neg_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) : ↑(-D) = -↑D

theorem LieDerivation.neg_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (a : L) : (-D) a = -D a

instance LieDerivation.instSub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Sub (LieDerivation R L M)

Equations

• LieDerivation.instSub = { sub := fun (D1 D2 : LieDerivation R L M) => { toLinearMap := ↑D1 - ↑D2, leibniz' := ⋯ } }

@[simp]

theorem LieDerivation.coe_sub {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 D2 : LieDerivation R L M) : ⇑(D1 - D2) = ⇑D1 - ⇑D2

@[simp]

theorem LieDerivation.coe_sub_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D1 D2 : LieDerivation R L M) : ↑(D1 - D2) = ↑D1 - ↑D2

theorem LieDerivation.sub_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (a : L) {D1 D2 : LieDerivation R L M} : (D1 - D2) a = D1 a - D2 a

class LieDerivation.SMulBracketCommClass (S : Type u_4) (L : Type u_5) (α : Type u_6) [SMul S α] [LieRing L] [AddCommGroup α] [LieRingModule L α] : Prop

A typeclass mixin saying that scalar multiplication and Lie bracket are left commutative.

• smul_bracket_comm (s : S) (l : L) (a : α) : s • ⁅l, a⁆ = ⁅l, s • a⁆

  • and ⁅⬝, ⬝⁆ are left commutative

instance LieDerivation.instSMul {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] : SMul S (LieDerivation R L M)

Equations

• LieDerivation.instSMul = { smul := fun (r : S) (D : LieDerivation R L M) => let __LinearMap := r • ↑D; { toLinearMap := __LinearMap, leibniz' := ⋯ } }

@[simp]

theorem LieDerivation.coe_smul {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) : ⇑(r • D) = r • ⇑D

@[simp]

theorem LieDerivation.coe_smul_linearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) : ↑(r • D) = r • ↑D

theorem LieDerivation.smul_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (a : L) {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) : (r • D) a = r • D a

instance LieDerivation.instSMulBase {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : SMulBracketCommClass R L M

instance LieDerivation.instSMulNat {L : Type u_2} {M : Type u_3} [LieRing L] [AddCommGroup M] [LieRingModule L M] : SMulBracketCommClass ℕ L M

instance LieDerivation.instSMulInt {L : Type u_2} {M : Type u_3} [LieRing L] [AddCommGroup M] [LieRingModule L M] : SMulBracketCommClass ℤ L M

instance LieDerivation.instAddCommGroup {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : AddCommGroup (LieDerivation R L M)

Equations

• LieDerivation.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def LieDerivation.coeFnAddMonoidHom {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieDerivation R L M →+ L → M

coe_fn as an AddMonoidHom.

Equations

• LieDerivation.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LieDerivation.coeFnAddMonoidHom_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) : coeFnAddMonoidHom D = ⇑D

instance LieDerivation.instDistribMulAction {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] : DistribMulAction S (LieDerivation R L M)

Equations

• LieDerivation.instDistribMulAction = Function.Injective.distribMulAction LieDerivation.coeFnAddMonoidHom ⋯ ⋯

instance LieDerivation.instIsScalarTower {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} {T : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] [Monoid T] [DistribMulAction T M] [SMulCommClass R T M] [SMulBracketCommClass T L M] [SMul S T] [IsScalarTower S T M] : IsScalarTower S T (LieDerivation R L M)

instance LieDerivation.instSMulCommClass {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} {T : Type u_5} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] [Monoid T] [DistribMulAction T M] [SMulCommClass R T M] [SMulBracketCommClass T L M] [SMulCommClass S T M] : SMulCommClass S T (LieDerivation R L M)

instance LieDerivation.instModule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] [SMulBracketCommClass S L M] : Module S (LieDerivation R L M)

Equations

• LieDerivation.instModule = Function.Injective.module S LieDerivation.coeFnAddMonoidHom ⋯ ⋯

instance LieDerivation.instBracket {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : Bracket (LieDerivation R L L) (LieDerivation R L L)

The commutator of two Lie derivations on a Lie algebra is a Lie derivation.

Equations

• LieDerivation.instBracket = { bracket := fun (D1 D2 : LieDerivation R L L) => { toLinearMap := ⁅↑D1, ↑D2⁆, leibniz' := ⋯ } }

@[simp]

theorem LieDerivation.commutator_coe_linear_map {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {D1 D2 : LieDerivation R L L} : ↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆

theorem LieDerivation.commutator_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {D1 D2 : LieDerivation R L L} (a : L) : ⁅D1, D2⁆ a = D1 (D2 a) - D2 (D1 a)

instance LieDerivation.instLieRing {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : LieRing (LieDerivation R L L)

Equations

• LieDerivation.instLieRing = { toAddCommGroup := LieDerivation.instAddCommGroup, toBracket := LieDerivation.instBracket, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

instance LieDerivation.instLieAlgebra {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra R (LieDerivation R L L)

The set of Lie derivations from a Lie algebra L to itself is a Lie algebra.

Equations

• LieDerivation.instLieAlgebra = { toModule := LieDerivation.instModule, lie_smul := ⋯ }

@[simp]

theorem LieDerivation.lie_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D₁ D₂ : LieDerivation R L L) (x : L) : ⁅D₁, D₂⁆ x = D₁ (D₂ x) - D₂ (D₁ x)

def LieDerivation.toLinearMapLieHom (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieDerivation R L L →ₗ⁅R⁆ L →ₗ[R] L

The Lie algebra morphism from Lie derivations into linear endormophisms.

Equations

• LieDerivation.toLinearMapLieHom R L = { toFun := LieDerivation.toLinearMap, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

theorem LieDerivation.toLinearMapLieHom_injective (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Injective ⇑(toLinearMapLieHom R L)

The map from Lie derivations to linear endormophisms is injective.

instance LieDerivation.instNoetherian (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : IsNoetherian R (LieDerivation R L L)

Lie derivations over a Noetherian Lie algebra form a Noetherian module.

def LieDerivation.inner (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : M →ₗ[R] LieDerivation R L M

The natural map from a Lie module to the derivations taking values in it.

Equations

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

@[simp]

theorem LieDerivation.inner_apply_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (m : M) (m✝ : L) : ((inner R L M) m) m✝ = ⁅m✝, m⁆

instance LieDerivation.instLieRingModule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieRingModule L (LieDerivation R L M)

Equations

• LieDerivation.instLieRingModule R L M = { bracket := fun (x : L) (D : LieDerivation R L M) => (LieDerivation.inner R L M) (D x), add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

@[simp]

theorem LieDerivation.lie_lieDerivation_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x y : L) (D : LieDerivation R L M) : ⁅x, D⁆ y = ⁅y, D x⁆

@[simp]

theorem LieDerivation.lie_coe_lieDerivation_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (D : LieDerivation R L M) : ⁅x, ↑D⁆ = ↑⁅x, D⁆

instance LieDerivation.instLieModule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule R L (LieDerivation R L M)

theorem LieDerivation.leibniz_lie (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (D₁ D₂ : LieDerivation R L L) : ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆

noncomputable def LieDerivation.exp {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra ℚ L] (D : LieDerivation R L L) (h : IsNilpotent ↑D) : L ≃ₗ⁅R⁆ L

In characteristic zero, the exponential of a nilpotent derivation is a Lie algebra automorphism.

Equations

• D.exp h = { toLinearMap := IsNilpotent.exp ↑D, map_lie' := ⋯, invFun := fun (x : L) => (IsNilpotent.exp (-↑D)) x, left_inv := ⋯, right_inv := ⋯ }

theorem LieDerivation.exp_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra ℚ L] (D : LieDerivation R L L) (h : IsNilpotent ↑D) : ↑(D.exp h).toLinearEquiv = IsNilpotent.exp ↑D

theorem LieDerivation.exp_map_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra ℚ L] (D : LieDerivation R L L) (h : IsNilpotent ↑D) (l : L) : (D.exp h) l = (IsNilpotent.exp ↑D) l