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.

Equations

Ring.instBracket = { bracket := fun (x y : A) => x * y - y * x }

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.

Equations

One or more equations did not get rendered due to their size.

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

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

Equations

One or more equations did not get rendered due to their size.

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.

Equations

LieAlgebra.ofAssociativeAlgebra = LieAlgebra.mk (_ : ∀ (t : R) (x y : A), ⁅x, t • y⁆ = t • ⁅x, y⁆)

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

Equations

Module.End.lieRingModule = LieRingModule.ofAssociativeModule

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

Equations

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

Equations

AlgHom.toLieHom f = let src := AlgHom.toLinearMap f; { toLinearMap := src, map_lie' := (_ : ∀ {x x_1 : A}, (AlgHom.toLinearMap f) (x * x_1 - x_1 * x) = f x * f x_1 - f x_1 * f x) }

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)

Equations

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

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

Equations

One or more equations did not get rendered due to their size.

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.

Equations

LieAlgebra.ad R L = LieModule.toEndomorphism 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 : 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 : ↥K} :

(LieModule.toEndomorphism R (↥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 (↥K) M) { val := x, property := hx } = (LieModule.toEndomorphism R L M) x

source

theorem LieSubmodule.coe_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) (y : ↥N) :

↑(((LieModule.toEndomorphism R L ↥↑N) x) y) = ((LieModule.toEndomorphism R L M) x) ↑y

source

theorem LieSubmodule.coe_toEndomorphism_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.toEndomorphism R L ↥↑N) x ^ n) y) = ((LieModule.toEndomorphism 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 : ↥H) (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 : ↥H) (y : ↥H) (n : ℕ) :

↑(((LieAlgebra.ad R ↥H) x ^ n) y) = ((LieAlgebra.ad R L) ↑x ^ n) ↑y

source

theorem LieModule.toEndomorphism_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 : L) (y : L) (z : M) :

((LieModule.toEndomorphism R L M) x) ⁅y, z⁆ = ⁅((LieAlgebra.ad R L) x) y, z⁆ + ⁅y, ((LieModule.toEndomorphism R L M) x) z⁆

source

theorem LieAlgebra.ad_lie (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) (z : L) :

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

source

theorem LieModule.toEndomorphism_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 : L) (y : L) (z : M) (n : ℕ) :

((LieModule.toEndomorphism R L M) x ^ n) ⁅y, z⁆ = Finset.sum (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => Nat.choose n ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieModule.toEndomorphism 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 : L) (y : L) (z : L) (n : ℕ) :

((LieAlgebra.ad R L) x ^ n) ⁅y, z⁆ = Finset.sum (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => Nat.choose n ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieAlgebra.ad R L) x ^ ij.2) z⁆

source

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

((LieModule.toEndomorphism R L M₂) x ^ k) ∘ₗ ↑f = ↑f ∘ₗ (LieModule.toEndomorphism R L M) x ^ k

source

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

((LieModule.toEndomorphism R L M₂) x ^ k) (f m) = f (((LieModule.toEndomorphism R L M) x ^ k) m)

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

((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), ((LieModule.toEndomorphism R L M) x ∘ₗ Submodule.subtype ↑N) { val := m, property := hm } ∈ ↑N) (_ : ∀ (m : M) (hm : m ∈ ↑N), ((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 ↥↑N) x

source

theorem LieSubmodule.mapsTo_pow_toEndomorphism_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.toEndomorphism 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] :

⇑(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 : ↥K) :

(LieAlgebra.ad R L) ↑x ∘ₗ ↑(LieSubalgebra.incl K) = ↑(LieSubalgebra.incl K) ∘ₗ (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

One or more equations did not get rendered due to their size.

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

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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

Documentation

Mathlib.Algebra.Lie.OfAssociative

Lie algebras of associative algebras #

Main definitions #

Tags #