# 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

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

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

Equations

- LieRing.ofAssociativeRing = { toAddCommGroup := inst✝.toAddCommGroup, toBracket := Ring.instBracket, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

source
theorem LieRing.of_associative_ring_bracket {A : Type v} [Ring A] (x y : A) :
⁅x, y⁆ = x * y - y * x
source
@[simp]
theorem LieRing.lie_apply {A : Type v} [Ring A] {α : Type u_1} (f g : α → A) (a : α) :
⁅f, g⁆ a = ⁅f a, g a⁆
source
@[reducible, inline]
abbrev LieRingModule.ofAssociativeModule {A : Type v} [Ring A] {M : Type w} [AddCommGroup M] [Module A M] :
LieRingModule 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 A`s:

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 = { bracket := fun (x1 : A) (x2 : M) => x1 • x2, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

Instances For

source
theorem lie_eq_smul {A : Type v} [Ring A] {M : Type w} [AddCommGroup M] [Module A M] (a : A) (m : M) :
⁅a, m⁆ = a • m
source
@[instance 100]
instance LieAlgebra.ofAssociativeAlgebra {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] :
LieAlgebra R A

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

Equations

- LieAlgebra.ofAssociativeAlgebra = { toModule := Algebra.toModule, lie_smul := ⋯ }

source
theorem LieModule.ofAssociativeModule {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {M : Type w} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R 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.

source
instance Module.End.instLieRingModule {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] :
LieRingModule (End R M) M
Equations

- Module.End.instLieRingModule = LieRingModule.ofAssociativeModule

source
instance Module.End.instLieModule {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] :
LieModule R (End R M) M
source
@[simp]
theorem Module.End.lie_apply {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] (f : End R M) (m : M) :
⁅f, m⁆ = f m
source
def AlgHom.toLieHom {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) :
A →ₗ⁅R⁆ B

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

Equations

- f.toLieHom = { toLinearMap := f.toLinearMap, map_lie' := ⋯ }

Instances For

source
instance AlgHom.instCoeLieHom {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] :
Coe (A →ₐ[R] B) (A →ₗ⁅R⁆ B)
Equations

- AlgHom.instCoeLieHom = { coe := AlgHom.toLieHom }

source
@[simp]
theorem AlgHom.coe_toLieHom {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) :
⇑f.toLieHom = ⇑f
source
theorem AlgHom.toLieHom_apply {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] (f : A →ₐ[R] B) (x : A) :
f.toLieHom x = f x
source
@[simp]
theorem AlgHom.toLieHom_id {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] :
(AlgHom.id R A).toLieHom = LieHom.id
source
@[simp]
theorem AlgHom.toLieHom_comp {A : Type v} [Ring A] {R : Type u} [CommRing R] [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
source
theorem AlgHom.toLieHom_injective {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] {B : Type w} [Ring B] [Algebra R B] {f g : A →ₐ[R] B} (h : f.toLieHom = g.toLieHom) :
f = g
source
def LieModule.toEnd (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
L →ₗ⁅R⁆ Module.End R M

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

See also `LieModule.toModuleHom`.

Equations

- LieModule.toEnd R L M = { toFun := fun (x : L) => { toFun := fun (m : M) => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source
@[simp]
theorem LieModule.toEnd_apply_apply (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) :
((toEnd R L M) x) m = ⁅x, m⁆
source
def LieAlgebra.ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
L →ₗ⁅R⁆ Module.End R L

The adjoint action of a Lie algebra on itself.

Equations

- LieAlgebra.ad R L = LieModule.toEnd R L L

Instances For

source
@[simp]
theorem LieAlgebra.ad_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) :
((ad R L) x) y = ⁅x, y⁆
source
@[simp]
theorem LieModule.toEnd_module_end (R : Type u) (M : Type w) [CommRing R] [AddCommGroup M] [Module R M] :
toEnd R (Module.End R M) M = LieHom.id
source
theorem LieSubalgebra.toEnd_eq (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (K : LieSubalgebra R L) {x : ↥K} :
(LieModule.toEnd R (↥K) M) x = (LieModule.toEnd R L M) ↑x
source
@[simp]
theorem LieSubalgebra.toEnd_mk (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (K : LieSubalgebra R L) {x : L} (hx : x ∈ K) :
(LieModule.toEnd R (↥K) M) ⟨x, hx⟩ = (LieModule.toEnd R L M) x
source
class LieModule.IsFaithful (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
Prop

A Lie module is faithful if the associated map `L → End M` is injective.

- injective_toEnd : Function.Injective ⇑(toEnd R L M)

Instances

source
theorem LieModule.isFaithful_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
IsFaithful R L M ↔ Function.Injective ⇑(toEnd R L M)
source
@[simp]
theorem LieModule.toEnd_eq_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsFaithful R L M] {x y : L} :
(toEnd R L M) x = (toEnd R L M) y ↔ x = y
source
theorem LieModule.ext_of_isFaithful {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsFaithful R L M] {x y : L} (h : ∀ (m : M), ⁅x, m⁆ = ⁅y, m⁆) :
x = y
source
@[simp]
theorem LieModule.toEnd_eq_zero_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsFaithful R L M] {x : L} :
(toEnd R L M) x = 0 ↔ x = 0
source
theorem LieModule.isFaithful_iff' (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
IsFaithful R L M ↔ ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
source
instance LieModule.instIsFaithfulSubtypeMemLieSubalgebra (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsFaithful R L M] {L' : LieSubalgebra R L} :
IsFaithful R (↥L') M
source
instance LieModule.instIsFaithfulEnd (R : Type u) (M : Type w) [CommRing R] [AddCommGroup M] [Module R M] :
IsFaithful R (Module.End R M) M
source
theorem LieSubmodule.coe_toEnd (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (y : ↥N) :
↑(((LieModule.toEnd R L ↥N) x) y) = ((LieModule.toEnd R L M) x) ↑y
source
theorem LieSubmodule.coe_toEnd_pow (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (y : ↥N) (n : ℕ) :
↑(((LieModule.toEnd R L ↥N) x ^ n) y) = ((LieModule.toEnd R L M) x ^ n) ↑y
source
theorem LieSubalgebra.coe_ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x y : ↥H) :
↑(((LieAlgebra.ad R ↥H) x) y) = ((LieAlgebra.ad R L) ↑x) ↑y
source
theorem LieSubalgebra.coe_ad_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x y : ↥H) (n : ℕ) :
↑(((LieAlgebra.ad R ↥H) x ^ n) y) = ((LieAlgebra.ad R L) ↑x ^ n) ↑y
source
theorem LieModule.toEnd_lie (R : Type u) {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x y : L) (z : M) :
((toEnd R L M) x) ⁅y, z⁆ = ⁅((LieAlgebra.ad R L) x) y, z⁆ + ⁅y, ((toEnd R L M) x) z⁆
source
theorem LieAlgebra.ad_lie (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x y z : L) :
((ad R L) x) ⁅y, z⁆ = ⁅((ad R L) x) y, z⁆ + ⁅y, ((ad R L) x) z⁆
source
theorem LieModule.toEnd_pow_lie (R : Type u) {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x y : L) (z : M) (n : ℕ) :
((toEnd R L M) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((toEnd R L M) x ^ ij.2) z⁆
source
theorem LieAlgebra.ad_pow_lie (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x y z : L) (n : ℕ) :
((ad R L) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, ((ad R L) x ^ ij.2) z⁆
source
theorem LieModule.toEnd_pow_comp_lieHom {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L⁆ M₂) (k : ℕ) (x : L) :
((toEnd R L M₂) x ^ k) ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x ^ k
source
theorem LieModule.toEnd_pow_apply_map {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L⁆ M₂) (k : ℕ) (x : L) (m : M) :
((toEnd R L M₂) x ^ k) (f m) = f (((toEnd R L M) x ^ k) m)
source
theorem LieSubmodule.coe_map_toEnd_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L M} {x : L} :
Submodule.map ((LieModule.toEnd R L M) x) ↑N ≤ ↑N
source
theorem LieSubmodule.toEnd_comp_subtype_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (m : M) (hm : m ∈ ↑N) :
((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N
source
@[simp]
theorem LieSubmodule.toEnd_restrict_eq_toEnd {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (h : ∀ (m : M) (hm : m ∈ ↑N), ((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N := ⋯) :
LinearMap.restrict ((LieModule.toEnd R L M) x) h = (LieModule.toEnd R L ↥N) x
source
theorem LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) {φ : R} {k : ℕ} {x : L} :
Set.MapsTo ⇑(((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) ↑N ↑N
source
theorem LieAlgebra.ad_eq_lmul_left_sub_lmul_right {R : Type u} [CommRing R] (A : Type v) [Ring A] [Algebra R A] :
⇑(ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R
source
theorem LieSubalgebra.ad_comp_incl_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (x : ↥K) :
(LieAlgebra.ad R L) ↑x ∘ₗ ↑K.incl = ↑K.incl ∘ₗ (LieAlgebra.ad R ↥K) x
source
def lieSubalgebraOfSubalgebra (R : Type u) [CommRing R] (A : Type v) [Ring A] [Algebra R A] (A' : Subalgebra R A) :
LieSubalgebra R A

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

Equations

- lieSubalgebraOfSubalgebra R A A' = { toSubmodule := Subalgebra.toSubmodule A', lie_mem' := ⋯ }

Instances For

source
def LinearEquiv.lieConj {R : Type u} {M₁ : Type v} {M₂ : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :
Module.End R M₁ ≃ₗ⁅R⁆ Module.End R M₂

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

Equations

- e.lieConj = { toLinearMap := ↑e.conj, map_lie' := ⋯, invFun := e.conj.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem LinearEquiv.lieConj_apply {R : Type u} {M₁ : Type v} {M₂ : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : Module.End R M₁) :
e.lieConj f = e.conj f
source
@[simp]
theorem LinearEquiv.lieConj_symm {R : Type u} {M₁ : Type v} {M₂ : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :
e.lieConj.symm = e.symm.lieConj
source
def AlgEquiv.toLieEquiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [CommRing R] [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 = { toFun := e.toFun, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯, invFun := e.toLinearEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem AlgEquiv.toLieEquiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [CommRing R] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
e.toLieEquiv x = e x
source
@[simp]
theorem AlgEquiv.toLieEquiv_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [CommRing R] [Ring A₁] [Ring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂) :
e.toLieEquiv.symm x = e.symm x
source
@[simp]
theorem LieAlgebra.conj_ad_apply {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') (x : L) :
e.toLinearEquiv.conj ((ad R L) x) = (ad R L') (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'`.