# mathlib3documentation

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 #

• 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 : invertible 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 : 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 : 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) :
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) :