# Lie algebras of associative algebras #

This file defines the Lie algebra structure that arises on an associative algebra via the ring commutator.

Since the linear endomorphisms of a Lie algebra form an associative algebra, one can define the adjoint action as a morphism of Lie algebras from a Lie algebra to its linear endomorphisms. We make such a definition in this file.

## Main definitions #

• LieAlgebra.ofAssociativeAlgebra
• LieAlgebra.ofAssociativeAlgebraHom
• LieModule.toEnd
• LieAlgebra.ad
• LinearEquiv.lieConj
• AlgEquiv.toLieEquiv

## Tags #

lie algebra, ring commutator, adjoint action

@[instance 100]
instance LieRing.ofAssociativeRing {A : Type v} [Ring A] :

An associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator.

Equations
theorem LieRing.of_associative_ring_bracket {A : Type v} [Ring A] (x : A) (y : A) :
x, y = x * y - y * x
@[simp]
theorem LieRing.lie_apply {A : Type v} [Ring A] {α : Type u_1} (f : αA) (g : αA) (a : α) :
f, g a = f a, g a
@[reducible, inline]
abbrev LieRingModule.ofAssociativeModule {A : Type v} [Ring A] {M : Type w} [] [Module A M] :

We can regard a module over an associative ring A as a Lie ring module over A with Lie bracket equal to its ring commutator.

Note that this cannot be a global instance because it would create a diamond when M = A, specifically we can build two mathematically-different bracket A As:

1. @Ring.bracket A _ which says ⁅a, b⁆ = a * b - b * a
2. (@LieRingModule.ofAssociativeModule A _ A _ _).toBracket which says ⁅a, b⁆ = a • b (and thus ⁅a, b⁆ = a * b)

See note [reducible non-instances]

Equations
• LieRingModule.ofAssociativeModule =
Instances For
theorem lie_eq_smul {A : Type v} [Ring A] {M : Type w} [] [Module A M] (a : A) (m : M) :
a, m = a m
@[instance 100]
instance LieAlgebra.ofAssociativeAlgebra {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] :

An associative algebra gives rise to a Lie algebra by taking the bracket to be the ring commutator.

Equations
• LieAlgebra.ofAssociativeAlgebra =
theorem LieModule.ofAssociativeModule {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] {M : Type w} [] [Module R M] [Module A M] [] :
LieModule R A M

A representation of an associative algebra A is also a representation of A, regarded as a Lie algebra via the ring commutator.

See the comment at LieRingModule.ofAssociativeModule for why the possibility M = A means this cannot be a global instance.

instance Module.End.instLieRingModule {R : Type u} [] {M : Type w} [] [Module R M] :
Equations
• Module.End.instLieRingModule = LieRingModule.ofAssociativeModule
instance Module.End.instLieModule {R : Type u} [] {M : Type w} [] [Module R M] :
LieModule R () M
Equations
• =
@[simp]
theorem Module.End.lie_apply {R : Type u} [] {M : Type w} [] [Module R M] (f : ) (m : M) :
f, m = f m
def AlgHom.toLieHom {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) :

The map ofAssociativeAlgebra associating a Lie algebra to an associative algebra is functorial.

Equations
• f.toLieHom = let __src := f.toLinearMap; { toLinearMap := __src, map_lie' := }
Instances For
instance AlgHom.instCoeLieHom {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] :
Coe (A →ₐ[R] B) (A →ₗ⁅R B)
Equations
• AlgHom.instCoeLieHom = { coe := AlgHom.toLieHom }
@[simp]
theorem AlgHom.coe_toLieHom {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) :
f.toLieHom = f
theorem AlgHom.toLieHom_apply {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) (x : A) :
f.toLieHom x = f x
@[simp]
theorem AlgHom.toLieHom_id {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] :
().toLieHom = LieHom.id
@[simp]
theorem AlgHom.toLieHom_comp {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] {B : Type w} {C : Type w₁} [Ring B] [Ring C] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
(g.comp f).toLieHom = g.toLieHom.comp f.toLieHom
theorem AlgHom.toLieHom_injective {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] {f : A →ₐ[R] B} {g : A →ₐ[R] B} (h : f.toLieHom = g.toLieHom) :
f = g
@[simp]
theorem LieModule.toEnd_apply_apply (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (m : M) :
(() x) m = x, m
def LieModule.toEnd (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :

A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module.

See also LieModule.toModuleHom.

Equations
• = { toFun := fun (x : L) => { toFun := fun (m : M) => x, m, map_add' := , map_smul' := }, map_add' := , map_smul' := , map_lie' := }
Instances For
def LieAlgebra.ad (R : Type u) (L : Type v) [] [] [] :

The adjoint action of a Lie algebra on itself.

Equations
Instances For
@[simp]
theorem LieAlgebra.ad_apply (R : Type u) (L : Type v) [] [] [] (x : L) (y : L) :
(() x) y = x, y
@[simp]
theorem LieModule.toEnd_module_end (R : Type u) (M : Type w) [] [] [Module R M] :
LieModule.toEnd R () M = LieHom.id
theorem LieSubalgebra.toEnd_eq (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (K : ) {x : K} :
(LieModule.toEnd R (K) M) x = () x
@[simp]
theorem LieSubalgebra.toEnd_mk (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (K : ) {x : L} (hx : x K) :
(LieModule.toEnd R (K) M) x, hx = () x
theorem LieSubmodule.coe_toEnd (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (y : N) :
(((LieModule.toEnd R L N) x) y) = (() x) y
theorem LieSubmodule.coe_toEnd_pow (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (y : N) (n : ) :
(((LieModule.toEnd R L N) x ^ n) y) = (() x ^ n) y
theorem LieSubalgebra.coe_ad (R : Type u) (L : Type v) [] [] [] (H : ) (x : H) (y : H) :
((() x) y) = (() x) y
theorem LieSubalgebra.coe_ad_pow (R : Type u) (L : Type v) [] [] [] (H : ) (x : H) (y : H) (n : ) :
((() x ^ n) y) = (() x ^ n) y
theorem LieModule.toEnd_lie (R : Type u) {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (y : L) (z : M) :
(() x) y, z = (() x) y, z + y, (() x) z
theorem LieAlgebra.ad_lie (R : Type u) {L : Type v} [] [] [] (x : L) (y : L) (z : L) :
(() x) y, z = (() x) y, z + y, (() x) z
theorem LieModule.toEnd_pow_lie (R : Type u) {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (y : L) (z : M) (n : ) :
(() x ^ n) y, z = ij, n.choose ij.1 (() x ^ ij.1) y, (() x ^ ij.2) z
theorem LieAlgebra.ad_pow_lie (R : Type u) {L : Type v} [] [] [] (x : L) (y : L) (z : L) (n : ) :
(() x ^ n) y, z = ij, n.choose ij.1 (() x ^ ij.1) y, (() x ^ ij.2) z
theorem LieModule.toEnd_pow_comp_lieHom {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type w₁} [] [Module R M₂] [] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) (k : ) (x : L) :
((LieModule.toEnd R L M₂) x ^ k) ∘ₗ f = f ∘ₗ () x ^ k
theorem LieModule.toEnd_pow_apply_map {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type w₁} [] [Module R M₂] [] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) (k : ) (x : L) (m : M) :
((LieModule.toEnd R L M₂) x ^ k) (f m) = f ((() x ^ k) m)
theorem LieSubmodule.coe_map_toEnd_le {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {N : LieSubmodule R L M} {x : L} :
Submodule.map (() x) N N
theorem LieSubmodule.toEnd_comp_subtype_mem {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (m : M) (hm : m N) :
(() x ∘ₗ (N).subtype) m, hm N
@[simp]
theorem LieSubmodule.toEnd_restrict_eq_toEnd {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (h : optParam (∀ (m : M) (hm : m N), (() x ∘ₗ (N).subtype) m, hm N) ) :
LinearMap.restrict (() x) h = (LieModule.toEnd R L N) x
theorem LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) {φ : R} {k : } {x : L} :
Set.MapsTo ((() x - (algebraMap R ()) φ) ^ k) N N
theorem LieAlgebra.ad_eq_lmul_left_sub_lmul_right {R : Type u} [] (A : Type v) [Ring A] [Algebra R A] :
() =
theorem LieSubalgebra.ad_comp_incl_eq {R : Type u} {L : Type v} [] [] [] (K : ) (x : K) :
() x ∘ₗ K.incl = K.incl ∘ₗ () x
def lieSubalgebraOfSubalgebra (R : Type u) [] (A : Type v) [Ring A] [Algebra R A] (A' : ) :

A subalgebra of an associative algebra is a Lie subalgebra of the associated Lie algebra.

Equations
• = let __src := Subalgebra.toSubmodule A'; { toSubmodule := __src, lie_mem' := }
Instances For
def LinearEquiv.lieConj {R : Type u} {M₁ : Type v} {M₂ : Type w} [] [] [Module R M₁] [] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :

A linear equivalence of two modules induces a Lie algebra equivalence of their endomorphisms.

Equations
• e.lieConj = let __src := e.conj; { toLinearMap := __src, map_lie' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.lieConj_apply {R : Type u} {M₁ : Type v} {M₂ : Type w} [] [] [Module R M₁] [] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : Module.End R M₁) :
e.lieConj f = e.conj f
@[simp]
theorem LinearEquiv.lieConj_symm {R : Type u} {M₁ : Type v} {M₂ : Type w} [] [] [Module R M₁] [] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :
e.lieConj.symm = e.symm.lieConj
def AlgEquiv.toLieEquiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
A₁ ≃ₗ⁅R A₂

An equivalence of associative algebras is an equivalence of associated Lie algebras.

Equations
• e.toLieEquiv = let __src := e.toLinearEquiv; { toFun := e.toFun, map_add' := , map_smul' := , map_lie' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem AlgEquiv.toLieEquiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
e.toLieEquiv x = e x
@[simp]
theorem AlgEquiv.toLieEquiv_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂) :
e.toLieEquiv.symm x = e.symm x
@[simp]
theorem LieAlgebra.conj_ad_apply {R : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R L') (x : L) :
e.toLinearEquiv.conj (() x) = () (e x)

Given an equivalence e of Lie algebras from L to L', and an element x : L, the conjugate of the endomorphism ad(x) of L by e is the endomorphism ad(e x) of L'.