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

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

Documentation

Mathlib.Algebra.Lie.OfAssociative

Lie algebras of associative algebras #

Main definitions #

Tags #