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 #
lie_equiv_matrix'matrix.lie_conjmatrix.reindex_lie_equiv
Tags #
lie algebra, matrix
def
lie_equiv_matrix'
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq 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.
Equations
- lie_equiv_matrix' = {to_lie_hom := {to_linear_map := {to_fun := linear_map.to_matrix'.to_fun, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := linear_map.to_matrix'.inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
lie_equiv_matrix'_apply
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(f : module.End R (n → R)) :
@[simp]
theorem
lie_equiv_matrix'_symm_apply
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(A : matrix n n R) :
def
matrix.lie_conj
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(P : matrix n n R)
(h : invertible P) :
An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself.
Equations
@[simp]
theorem
matrix.lie_conj_apply
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(P A : matrix n n R)
(h : invertible P) :
@[simp]
theorem
matrix.lie_conj_symm_apply
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(P A : matrix n n R)
(h : invertible P) :
def
matrix.reindex_lie_equiv
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
{m : Type w₁}
[decidable_eq m]
[fintype m]
(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.
Equations
- matrix.reindex_lie_equiv e = {to_lie_hom := {to_linear_map := {to_fun := ⇑(matrix.reindex e e), map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := (matrix.reindex_linear_equiv R R e e).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
matrix.reindex_lie_equiv_apply
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
{m : Type w₁}
[decidable_eq m]
[fintype m]
(e : n ≃ m)
(M : matrix n n R) :
⇑(matrix.reindex_lie_equiv e) M = ⇑(matrix.reindex e e) M
@[simp]
theorem
matrix.reindex_lie_equiv_symm
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
{m : Type w₁}
[decidable_eq m]
[fintype m]
(e : n ≃ m) :