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 LinearMap :

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⁆

Instances For

source

theorem LieDerivation.leibniz' {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] (self : LieDerivation R L M) (a : L) (b : L) :

↑self ⁅a, b⁆ = ⁅a, ↑self b⁆ - ⁅b, ↑self a⁆

source

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' := ⋯ }

source

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

Equations

⋯ = ⋯

source

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

source

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

source

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 }

source

@[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

source

@[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

source

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

source

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 : LieDerivation R L M} {D2 : LieDerivation R L M} :

D1 = D2 ↔ ∀ (a : L), D1 a = D2 a

source

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 : LieDerivation R L M} {D2 : LieDerivation R L M} (H : ∀ (a : L), D1 a = D2 a) :

D1 = D2

source

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 : LieDerivation R L M} {D2 : LieDerivation R L M} (h : D1 = D2) (a : L) :

D1 a = D2 a

source

@[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 : L) (b : L) :

D ⁅a, b⁆ = ⁅a, D b⁆ - ⁅b, D a⁆

source

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 : L) (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.

source

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 : LieDerivation R L M} {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.

source

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 : LieDerivation R L M} {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.

source

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 : L) (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.

source

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 : L) (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.

source

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 := { toLinearMap := 0, leibniz' := ⋯ } }

source

@[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

source

@[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

source

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

source

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 }

source

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) => { toLinearMap := ↑D1 + ↑D2, leibniz' := ⋯ } }

source

@[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 : LieDerivation R L M) (D2 : LieDerivation R L M) :

⇑(D1 + D2) = ⇑D1 + ⇑D2

source

@[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 : LieDerivation R L M) (D2 : LieDerivation R L M) :

↑(D1 + D2) = ↑D1 + ↑D2

source

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 : LieDerivation R L M} {D2 : LieDerivation R L M} (a : L) :

(D1 + D2) a = D1 a + D2 a

source

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

source

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 : L) (b : L) :

D (a - b) = D a - D b

source

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' := ⋯ } }

source

@[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

source

@[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

source

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

source

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' := ⋯ } }

source

@[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 : LieDerivation R L M) (D2 : LieDerivation R L M) :

⇑(D1 - D2) = ⇑D1 - ⇑D2

source

@[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 : LieDerivation R L M) (D2 : LieDerivation R L M) :

↑(D1 - D2) = ↑D1 - ↑D2

source

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 : LieDerivation R L M} {D2 : LieDerivation R L M} :

(D1 - D2) a = D1 a - D2 a

source

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

Instances

source

theorem LieDerivation.SMulBracketCommClass.smul_bracket_comm {S : Type u_4} {L : Type u_5} {α : Type u_6} [SMul S α] [LieRing L] [AddCommGroup α] [LieRingModule L α] [self : LieDerivation.SMulBracketCommClass S L α] (s : S) (l : L) (a : α) :

s • ⁅l, a⁆ = ⁅l, s • a⁆

• and ⁅⬝, ⬝⁆ are left commutative

source

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] [LieDerivation.SMulBracketCommClass S L M] :

SMul S (LieDerivation R L M)

Equations

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

source

@[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] [LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) :

⇑(r • D) = r • ⇑D

source

@[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] [LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) :

↑(r • D) = r • ↑D

source

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] [LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M) :

(r • D) a = r • D a

source

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] :

LieDerivation.SMulBracketCommClass R L M

Equations

⋯ = ⋯

source

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

LieDerivation.SMulBracketCommClass ℕ L M

Equations

⋯ = ⋯

source

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

LieDerivation.SMulBracketCommClass ℤ L M

Equations

⋯ = ⋯

source

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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' := ⋯ }

source

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] [LieDerivation.SMulBracketCommClass S L M] :

DistribMulAction S (LieDerivation R L M)

Equations

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

source

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] [LieDerivation.SMulBracketCommClass S L M] [Monoid T] [DistribMulAction T M] [SMulCommClass R T M] [LieDerivation.SMulBracketCommClass T L M] [SMul S T] [IsScalarTower S T M] :

IsScalarTower S T (LieDerivation R L M)

Equations

⋯ = ⋯

source

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] [LieDerivation.SMulBracketCommClass S L M] [Monoid T] [DistribMulAction T M] [SMulCommClass R T M] [LieDerivation.SMulBracketCommClass T L M] [SMulCommClass S T M] :

SMulCommClass S T (LieDerivation R L M)

Equations

⋯ = ⋯

source

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] [LieDerivation.SMulBracketCommClass S L M] :

Module S (LieDerivation R L M)

Equations

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

source

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' := ⋯ } }

source

@[simp]

theorem LieDerivation.commutator_coe_linear_map {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {D1 : LieDerivation R L L} {D2 : LieDerivation R L L} :

↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆

source

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

⁅D1, D2⁆ a = D1 (D2 a) - D2 (D1 a)

source

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 = LieRing.mk ⋯ ⋯ ⋯ ⋯

source

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 = LieAlgebra.mk ⋯

source

@[simp]

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

⁅D₁, D₂⁆ x = D₁ (D₂ x) - D₂ (D₁ x)

source

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' := ⋯ }

source

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

Function.Injective ⇑(LieDerivation.toLinearMapLieHom R L)

The map from Lie derivations to linear endormophisms is injective.

source

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.

Equations

⋯ = ⋯

source

@[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) :

((LieDerivation.inner R L M) m✝) m = ⁅m, m✝⁆

source

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.

source

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 = LieRingModule.mk ⋯ ⋯ ⋯

source

@[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 : L) (y : L) (D : LieDerivation R L M) :

⁅x, D⁆ y = ⁅y, D x⁆

source

@[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⁆

source

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)

Equations

⋯ = ⋯

source

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

⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆

Documentation

Mathlib.Algebra.Lie.Derivation.Basic

Lie derivations #

Main definitions #

Main statements #

Implementation notes #