mathlibdocumentation

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 #

• lie_equiv_matrix'
• matrix.lie_conj
• matrix.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] :
(n → R) ≃ₗ⁅R n R

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

Equations
@[simp]
theorem lie_equiv_matrix'_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (f : (n → R)) :
@[simp]
theorem lie_equiv_matrix'_symm_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (A : n R) :
def matrix.lie_conj {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (P : n R) (h : is_unit P) :
n R ≃ₗ⁅R n R

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 : n R) (h : is_unit P) :
(P.lie_conj h) A = P A P⁻¹
@[simp]
theorem matrix.lie_conj_symm_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (P A : n R) (h : is_unit P) :
((P.lie_conj h).symm) A = P⁻¹ A 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) :
n R ≃ₗ⁅R 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.

Equations
@[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 : n R) :
= 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) :