mathlib3 documentation

algebra.lie.matrix

Lie algebras of matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] :

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

Equations
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) :
(P.lie_conj h) A = (P.mul A).mul 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) :
((P.lie_conj h).symm) A = (P⁻¹.mul A).mul 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) :