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

source

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 := _}

source

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

⇑lie_equiv_matrix' f = ⇑linear_map.to_matrix' f

source

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

⇑(lie_equiv_matrix'.symm) A = ⇑matrix.to_lin' A

source

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

matrix n n R ≃ₗ⁅R⁆ matrix n n R

An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself.

Equations

P.lie_conj h = (lie_equiv_matrix'.symm.trans (P.to_linear_equiv' h).lie_conj).trans lie_equiv_matrix'

source

@[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⁻¹

source

@[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

source

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

matrix n n R ≃ₗ⁅R⁆ matrix m 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

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 := _}

source

@[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

source

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

(matrix.reindex_lie_equiv e).symm = matrix.reindex_lie_equiv e.symm