# Documentation

Mathlib.Algebra.Lie.OfAssociative

# 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.toEndomorphism
• LieAlgebra.ad
• LinearEquiv.lieConj
• AlgEquiv.toLieEquiv

## Tags #

lie algebra, ring commutator, adjoint action

instance Ring.instBracket {A : Type v} [Ring A] :

The bracket operation for rings is the ring commutator, which captures the extent to which a ring is commutative. It is identically zero exactly when the ring is commutative.

theorem Ring.lie_def {A : Type v} [Ring A] (x : A) (y : A) :
x, y = x * y - y * x
theorem commute_iff_lie_eq {A : Type v} [Ring A] {x : A} {y : A} :
Commute x y x, y = 0
theorem Commute.lie_eq {A : Type v} [Ring A] {x : A} {y : A} (h : Commute x y) :
x, y = 0
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.

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 : α) :
αA, αA LieRingModule.toBracket f g a = f a, g a
@[reducible]
def 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]

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

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.lieRingModule {R : Type u} [] {M : Type w} [] [Module R M] :
instance Module.End.lieModule {R : Type u} [] {M : Type w} [] [Module R M] :
LieModule R () 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.

Instances For
@[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
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) :
↑() x = f x
@[simp]
theorem AlgHom.toLieHom_id {A : Type v} [Ring A] {R : Type u} [] [Algebra R A] :
AlgHom.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) :
=
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 = g
@[simp]
theorem LieModule.toEndomorphism_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.toEndomorphism (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.

Instances For
def LieAlgebra.ad (R : Type u) (L : Type v) [] [] [] :

The adjoint action of a Lie algebra on itself.

Instances For
@[simp]
theorem LieAlgebra.ad_apply (R : Type u) (L : Type v) [] [] [] (x : L) (y : L) :
↑(↑() x) y = x, y
@[simp]
theorem LieModule.toEndomorphism_module_end (R : Type u) (M : Type w) [] [] [Module R M] :
= LieHom.id
theorem LieSubalgebra.toEndomorphism_eq (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (K : ) {x : { x // x K }} :
↑(LieModule.toEndomorphism R { x // x K } M) x = ↑() x
@[simp]
theorem LieSubalgebra.toEndomorphism_mk (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (K : ) {x : L} (hx : x K) :
↑(LieModule.toEndomorphism R { x // x K } M) { val := x, property := hx } = ↑() x
theorem LieSubmodule.coe_map_toEndomorphism_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.toEndomorphism_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) :
↑(LinearMap.comp (↑() x) ()) { val := m, property := hm } N
@[simp]
theorem LieSubmodule.toEndomorphism_restrict_eq_toEndomorphism {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), ↑(LinearMap.comp (↑() x) ()) { val := m, property := hm } N) (_ : ∀ (m : M) (hm : m N), ↑(LinearMap.comp (↑() x) ()) { val := m, property := hm } N)) :
LinearMap.restrict (↑() x) h = ↑(LieModule.toEndomorphism R L { x // x N }) x
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 : { x // x K }) :
LinearMap.comp (↑() x) ↑() = LinearMap.comp (↑()) (↑(LieAlgebra.ad R { x // x K }) 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.

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.

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₁) :
↑() f = ↑() 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₂) :
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.

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₁) :
↑() 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₂) :
↑() x = ↑() x