# Documentation

Mathlib.Algebra.Lie.Matrix

# 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} [] {n : Type w} [] [] :
Module.End R (nR) ≃ₗ⁅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.

Instances For
@[simp]
theorem lieEquivMatrix'_apply {R : Type u} [] {n : Type w} [] [] (f : Module.End R (nR)) :
lieEquivMatrix' f = LinearMap.toMatrix' f
@[simp]
theorem lieEquivMatrix'_symm_apply {R : Type u} [] {n : Type w} [] [] (A : Matrix n n R) :
↑(LieEquiv.symm lieEquivMatrix') A = Matrix.toLin' A
def Matrix.lieConj {R : Type u} [] {n : Type w} [] [] (P : Matrix n n R) (h : ) :

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

Instances For
@[simp]
theorem Matrix.lieConj_apply {R : Type u} [] {n : Type w} [] [] (P : Matrix n n R) (A : Matrix n n R) (h : ) :
↑() A = P * A * P⁻¹
@[simp]
theorem Matrix.lieConj_symm_apply {R : Type u} [] {n : Type w} [] [] (P : Matrix n n R) (A : Matrix n n R) (h : ) :
↑() A = P⁻¹ * A * P
def Matrix.reindexLieEquiv {R : Type u} [] {n : Type w} [] [] {m : Type w₁} [] [] (e : n m) :

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.

Instances For
@[simp]
theorem Matrix.reindexLieEquiv_apply {R : Type u} [] {n : Type w} [] [] {m : Type w₁} [] [] (e : n m) (M : Matrix n n R) :
↑() M = ↑() M
@[simp]
theorem Matrix.reindexLieEquiv_symm {R : Type u} [] {n : Type w} [] [] {m : Type w₁} [] [] (e : n m) :