Lie algebras of matrices

An important class of Lie algebras are those arising from the associative algebra structure on square matrices over a commutative ring. This file provides some very basic definitions whose primary value stems from their utility when constructing the classical Lie algebras using matrices.

Main definitions

• lieEquivMatrix'
• Matrix.lieConj
• Matrix.reindexLieEquiv

Tags

lie algebra, matrix

def lieEquivMatrix' {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] : Module.End R (n → R) ≃ₗ⁅R⁆ Matrix n n R

The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the Lie algebra structures.

@[simp]

theorem lieEquivMatrix'_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (f : Module.End R (n → R)) : lieEquivMatrix' f = LinearMap.toMatrix' f

@[simp]

theorem lieEquivMatrix'_symm_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (A : Matrix n n R) : lieEquivMatrix'.symm A = Matrix.toLin' A

def Matrix.lieConj {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (P : Matrix n n R) (h : Invertible P) : Matrix n n R ≃ₗ⁅R⁆ Matrix n n R

An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself.

@[simp]

theorem Matrix.lieConj_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (P A : Matrix n n R) (h : Invertible P) : (P.lieConj h) A = P * A * P⁻¹

@[simp]

theorem Matrix.lieConj_symm_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (P A : Matrix n n R) (h : Invertible P) : (P.lieConj h).symm A = P⁻¹ * A * P

def Matrix.reindexLieEquiv {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type w₁} [DecidableEq m] [Fintype m] (e : n ≃ m) : Matrix n n R ≃ₗ⁅R⁆ Matrix m m R

For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent types, Matrix.reindex, is an equivalence of Lie algebras.

@[simp]

theorem Matrix.reindexLieEquiv_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type w₁} [DecidableEq m] [Fintype m] (e : n ≃ m) (M : Matrix n n R) : (reindexLieEquiv e) M = (reindex e e) M

@[simp]

theorem Matrix.reindexLieEquiv_symm {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type w₁} [DecidableEq m] [Fintype m] (e : n ≃ m) : (reindexLieEquiv e).symm = reindexLieEquiv e.symm

instance Matrix.instLieRingModuleForall {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] : LieRingModule (Matrix n n R) (n → R)

instance Matrix.instLieModuleForall {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] : LieModule R (Matrix n n R) (n → R)

@[simp]

theorem Matrix.lie_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (A : Matrix n n R) (v : n → R) : ⁅A, v⁆ = A.mulVec v

@[simp]

theorem LieModule.toEnd_matrix {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] : toEnd R (Matrix n n R) (n → R) = lieEquivMatrix'.symm.toLieHom

instance LieModule.instIsFaithfulMatrixForall {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] : IsFaithful R (Matrix n n R) (n → R)