mathlib documentation

algebra.lie.of_associative

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 #

Tags #

lie algebra, ring commutator, adjoint action

@[instance]
def ring.has_bracket {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.

Equations
theorem ring.lie_def {A : Type v} [ring A] (x y : A) :
x,y = x * y - y * x
@[instance]
def lie_ring.of_associative_ring {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 lie_ring.of_associative_ring_bracket {A : Type v} [ring A] (x y : A) :
x,y = x * y - y * x
@[instance]
def lie_algebra.of_associative_algebra {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] :

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

Equations
def lie_algebra.of_associative_algebra_hom {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] (f : A →ₐ[R] B) :

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

Equations
@[simp]
theorem lie_algebra.of_associative_algebra_hom_apply {A : Type v} [ring A] {R : Type u} [comm_ring R] [algebra R A] {B : Type w} [ring B] [algebra R B] (f : A →ₐ[R] B) (x : A) :
@[simp]
theorem lie_algebra.of_associative_algebra_hom_comp {A : Type v} [ring A] {R : Type u} [comm_ring 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) :
def lie_module.to_endomorphism (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

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

Equations
@[simp]
theorem lie_module.to_endomorphism_apply_apply (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (x : L) (m : M) :
def lie_algebra.ad (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

The adjoint action of a Lie algebra on itself.

Equations
@[simp]
theorem lie_algebra.ad_apply (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (x y : L) :
def lie_subalgebra_of_subalgebra (R : Type u) [comm_ring R] (A : Type v) [ring A] [algebra R A] (A' : subalgebra R A) :

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

Equations
def linear_equiv.lie_conj {R : Type u} {M₁ : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (e : M₁ ≃ₗ[R] M₂) :

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

Equations
@[simp]
theorem linear_equiv.lie_conj_apply {R : Type u} {M₁ : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : module.End R M₁) :
(e.lie_conj) f = (e.conj) f
@[simp]
theorem linear_equiv.lie_conj_symm {R : Type u} {M₁ : Type v} {M₂ : Type w} [comm_ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (e : M₁ ≃ₗ[R] M₂) :
def alg_equiv.to_lie_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring 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
@[simp]
theorem alg_equiv.to_lie_equiv_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
@[simp]
theorem alg_equiv.to_lie_equiv_symm_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂) :