mathlib documentation

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 #

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
@[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 : is_unit 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 : 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 : matrix n 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) :

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