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

@[implicit_reducible, 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 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]

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

@[implicit_reducible, 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

@[implicit_reducible]

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

theorem Module.End.instLieRingModule_eq {R : Type u} [CommRing R] {M : Type w} [AddCommGroup M] [Module R M] :

LinearMap.instLieRingModule = lieRingSelfModule

Unfortunately we now have two brackets which are not equal at reducible transparency, even though they are equal at default transparency. We can use this lemma on rare occasions when this matters.

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

@[implicit_reducible]

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

Documentation

Mathlib.Algebra.Lie.OfAssociative

Lie algebras of associative algebras #

Main definitions #

Tags #