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

source

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

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

source

theorem Ring.lie_def {A : Type v} [Ring A] (x : A) (y : A) :

⁅x, y⁆ = x * y - y * x

source

theorem commute_iff_lie_eq {A : Type v} [Ring A] {x : A} {y : A} :

Commute x y ↔ ⁅x, y⁆ = 0

source

theorem Commute.lie_eq {A : Type v} [Ring A] {x : A} {y : A} (h : Commute x y) :

⁅x, y⁆ = 0

source

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.

source

theorem LieRing.of_associative_ring_bracket {A : Type v} [Ring A] (x : A) (y : A) :

⁅x, y⁆ = x * y - y * x

source

@[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⁆

source

@[reducible]

def 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 As:

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

See note [reducible non-instances]

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

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.lieRingModule {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] :

LieRingModule (Module.End R M) M

source

instance Module.End.lieModule {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] :

LieModule R (Module.End R M) 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.

Instances For

source

instance AlgHom.instCoeAlgHomToCommSemiringToSemiringToSemiringLieHomOfAssociativeRingOfAssociativeAlgebraOfAssociativeRingOfAssociativeAlgebra {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)

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) :

↑(AlgHom.toLieHom f) = ↑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) :

↑(AlgHom.toLieHom f) x = ↑f x

source

@[simp]

theorem AlgHom.toLieHom_id {A : Type v} [Ring A] {R : Type u} [CommRing R] [Algebra R A] :

AlgHom.toLieHom (AlgHom.id R A) = 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) :

AlgHom.toLieHom (AlgHom.comp g f) = LieHom.comp (AlgHom.toLieHom g) (AlgHom.toLieHom f)

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 : A →ₐ[R] B} {g : A →ₐ[R] B} (h : AlgHom.toLieHom f = AlgHom.toLieHom g) :

f = g

source

@[simp]

theorem LieModule.toEndomorphism_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) :

↑(↑(LieModule.toEndomorphism R L M) x) m = ⁅x, m⁆

source

def LieModule.toEndomorphism (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.

Instances For

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.

Instances For

source

@[simp]

theorem LieAlgebra.ad_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) :

↑(↑(LieAlgebra.ad R L) x) y = ⁅x, y⁆

source

@[simp]

theorem LieModule.toEndomorphism_module_end (R : Type u) (M : Type w) [CommRing R] [AddCommGroup M] [Module R M] :

LieModule.toEndomorphism R (Module.End R M) M = LieHom.id

source

theorem LieSubalgebra.toEndomorphism_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 : { x // x ∈ K }} :

↑(LieModule.toEndomorphism R { x // x ∈ K } M) x = ↑(LieModule.toEndomorphism R L M) ↑x

source

@[simp]

theorem LieSubalgebra.toEndomorphism_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.toEndomorphism R { x // x ∈ K } M) { val := x, property := hx } = ↑(LieModule.toEndomorphism R L M) x

source

theorem LieSubmodule.coe_map_toEndomorphism_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.toEndomorphism R L M) x) ↑N ≤ ↑N

source

theorem LieSubmodule.toEndomorphism_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) :

↑(LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N

source

@[simp]

theorem LieSubmodule.toEndomorphism_restrict_eq_toEndomorphism {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 : optParam (∀ (m : M) (hm : m ∈ ↑N), ↑(LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N) (_ : ∀ (m : M) (hm : m ∈ ↑N), ↑(LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)) :

LinearMap.restrict (↑(LieModule.toEndomorphism R L M) x) h = ↑(LieModule.toEndomorphism R L { x // x ∈ ↑N }) x

source

theorem LieAlgebra.ad_eq_lmul_left_sub_lmul_right {R : Type u} [CommRing R] (A : Type v) [Ring A] [Algebra R A] :

↑(LieAlgebra.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 : { x // x ∈ K }) :

LinearMap.comp (↑(LieAlgebra.ad R L) ↑x) ↑(LieSubalgebra.incl K) = LinearMap.comp (↑(LieSubalgebra.incl K)) (↑(LieAlgebra.ad R { x // x ∈ 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.

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.

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₁) :

↑(LinearEquiv.lieConj e) f = ↑(LinearEquiv.conj e) 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₂) :

LieEquiv.symm (LinearEquiv.lieConj e) = LinearEquiv.lieConj (LinearEquiv.symm e)

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.

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₁) :

↑(AlgEquiv.toLieEquiv e) 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₂) :

↑(LieEquiv.symm (AlgEquiv.toLieEquiv e)) x = ↑(AlgEquiv.symm e) x