HepLean Documentation

Mathlib.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

source
def lieEquivMatrix' {R : Type u} [CommRing R] {n : Type w} [DecidableEq 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
  • lieEquivMatrix' = { toLinearMap := ↑LinearMap.toMatrix', map_lie' := ⋯, invFun := LinearMap.toMatrix'.invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
    source
    @[simp]
    theorem lieEquivMatrix'_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (f : Module.End R (n → R)) :
    lieEquivMatrix' f = LinearMap.toMatrix' f
    source
    @[simp]
    theorem lieEquivMatrix'_symm_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (A : Matrix n n R) :
    lieEquivMatrix'.symm A = Matrix.toLin' A
    source
    def Matrix.lieConj {R : Type u} [CommRing R] {n : Type w} [DecidableEq 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.lieConj h = (lieEquivMatrix'.symm.trans (P.toLinearEquiv' h).lieConj).trans lieEquivMatrix'
    Instances For
      source
      @[simp]
      theorem Matrix.lieConj_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (P : Matrix n n R) (A : Matrix n n R) (h : Invertible P) :
      (P.lieConj h) A = P * A * P⁻¹
      source
      @[simp]
      theorem Matrix.lieConj_symm_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (P : Matrix n n R) (A : Matrix n n R) (h : Invertible P) :
      (P.lieConj h).symm A = P⁻¹ * A * P
      source
      def Matrix.reindexLieEquiv {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type w₁} [DecidableEq 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
      Instances For
        source
        @[simp]
        theorem Matrix.reindexLieEquiv_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type w₁} [DecidableEq m] [Fintype m] (e : n ≃ m) (M : Matrix n n R) :
        (Matrix.reindexLieEquiv e) M = (Matrix.reindex e e) M
        source
        @[simp]
        theorem Matrix.reindexLieEquiv_symm {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type w₁} [DecidableEq m] [Fintype m] (e : n ≃ m) :
        (Matrix.reindexLieEquiv e).symm = Matrix.reindexLieEquiv e.symm