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

Main statements #

Two Lie derivations equal on a set are equal on its Lie span.
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 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 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' : ∀ (r : R) (x : L), self.toFun (r • x) = (RingHom.id R) r • self.toFun x
leibniz' : ∀ (a b : L), ↑self ⁅a, b⁆ = ⁅a, ↑self b⁆ - ⁅b, ↑self a⁆

Instances For

source

instance LieDerivation.instFunLikeLieDerivation {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.instFunLikeLieDerivation = { 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

Instances For

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

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.instInhabitedLieDerivation {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.instInhabitedLieDerivation = { 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

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.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 = { toZeroHom := { toFun := DFunLike.coe, map_zero' := ⋯ }, map_add' := ⋯ }

Instances For

source

instance LieDerivation.instDistribMulActionLieDerivationToAddMonoidToSubNegMonoidToAddGroupInstAddCommGroup {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.instDistribMulActionLieDerivationToAddMonoidToSubNegMonoidToAddGroupInstAddCommGroup = Function.Injective.distribMulAction LieDerivation.coeFnAddMonoidHom ⋯ ⋯

source

instance LieDerivation.instIsScalarTowerLieDerivationInstSMulInstSMul {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.instSMulCommClassLieDerivationInstSMulInstSMul {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.instLieRingLieDerivationToAddCommGroupToModuleLieRingSelfModuleLieAlgebraSelfModule {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] :

LieRing (LieDerivation R L L)

Equations

LieDerivation.instLieRingLieDerivationToAddCommGroupToModuleLieRingSelfModuleLieAlgebraSelfModule = LieRing.mk ⋯ ⋯ ⋯ ⋯

source

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

LieDerivation.SMulBracketCommClass R L L

Equations

⋯ = ⋯

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 ⋯

Documentation

Mathlib.Algebra.Lie.Derivation.Basic

Lie derivations #

Main definitions #

Main statements #

Implementation notes #