Classical Lie algebras

This file is the place to find definitions and basic properties of the classical Lie algebras:

• Aₗ = sl(l+1)
• Bₗ ≃ so(l+1, l) ≃ so(2l+1)
• Cₗ = sp(l)
• Dₗ ≃ so(l, l) ≃ so(2l)

Main definitions

• LieAlgebra.SpecialLinear.sl
• LieAlgebra.Symplectic.sp
• LieAlgebra.Orthogonal.so
• LieAlgebra.Orthogonal.so'
• LieAlgebra.Orthogonal.soIndefiniteEquiv
• LieAlgebra.Orthogonal.typeD
• LieAlgebra.Orthogonal.typeB
• LieAlgebra.Orthogonal.typeDEquivSo'
• LieAlgebra.Orthogonal.typeBEquivSo'

Implementation notes

Matrices or endomorphisms

Given a finite type and a commutative ring, the corresponding square matrices are equivalent to the endomorphisms of the corresponding finite-rank free module as Lie algebras, see lieEquivMatrix'. We can thus define the classical Lie algebras as Lie subalgebras either of matrices or of endomorphisms. We have opted for the former. At the time of writing (August 2020) it is unclear which approach should be preferred so the choice should be assumed to be somewhat arbitrary.

Diagonal quadratic form or diagonal Cartan subalgebra

For the algebras of type B and D, there are two natural definitions. For example since the 2l × 2l matrix: $$ J = \left[\begin{array}{cc} 0_l & 1_l\\ 1_l & 0_l \end{array}\right] $$ defines a symmetric bilinear form equivalent to that defined by the identity matrix I, we can define the algebras of type D to be the Lie subalgebra of skew-adjoint matrices either for J or for I. Both definitions have their advantages (in particular the J-skew-adjoint matrices define a Lie algebra for which the diagonal matrices form a Cartan subalgebra) and so we provide both. We thus also provide equivalences typeDEquivSo', soIndefiniteEquiv which show the two definitions are equivalent. Similarly for the algebras of type B.

Tags

classical lie algebra, special linear, symplectic, orthogonal

@[simp]

theorem LieAlgebra.matrix_trace_commutator_zero (n : Type u_1) (R : Type u₂) [DecidableEq n] [CommRing R] [Fintype n] (X Y : Matrix n n R) : ⁅X, Y⁆.trace = 0

def LieAlgebra.SpecialLinear.sl (n : Type u_1) (R : Type u₂) [DecidableEq n] [CommRing R] [Fintype n] : LieSubalgebra R (Matrix n n R)

The special linear Lie algebra: square matrices of trace zero.

theorem LieAlgebra.SpecialLinear.sl_bracket (n : Type u_1) (R : Type u₂) [DecidableEq n] [CommRing R] [Fintype n] (A B : ↥(sl n R)) : ↑⁅A, B⁆ = ↑A * ↑B - ↑B * ↑A

def LieAlgebra.SpecialLinear.single {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j : n) (h : i ≠ j) : R →ₗ[R] ↥(sl n R)

When i ≠ j, the single-element matrices are elements of sl n R.

Along with some elements produced by singleSubSingle, these form a natural basis of sl n R.

@[deprecated LieAlgebra.SpecialLinear.single (since := "2025-05-06")]

def LieAlgebra.SpecialLinear.Eb {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j : n) (h : i ≠ j) : R →ₗ[R] ↥(sl n R)

Alias of LieAlgebra.SpecialLinear.single.

---

When i ≠ j, the single-element matrices are elements of sl n R.

Along with some elements produced by singleSubSingle, these form a natural basis of sl n R.

@[simp]

theorem LieAlgebra.SpecialLinear.val_single {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j : n) (h : i ≠ j) (r : R) : ↑((single i j h) r) = Matrix.single i j r

@[deprecated LieAlgebra.SpecialLinear.val_single (since := "2025-05-06")]

theorem LieAlgebra.SpecialLinear.eb_val {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j : n) (h : i ≠ j) (r : R) : ↑((single i j h) r) = Matrix.single i j r

Alias of LieAlgebra.SpecialLinear.val_single.

def LieAlgebra.SpecialLinear.singleSubSingle {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j : n) : R →ₗ[R] ↥(sl n R)

The matrices with matching positive and negative elements on the diagonal are elements of sl n R. Along with single, a subset of these form a basis for sl n R.

@[simp]

theorem LieAlgebra.SpecialLinear.val_singleSubSingle {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j : n) (r : R) : ↑((singleSubSingle i j) r) = Matrix.single i i r - Matrix.single j j r

@[simp]

theorem LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j k : n) (r : R) : (singleSubSingle i j) r + (singleSubSingle j k) r = (singleSubSingle i k) r

@[simp]

theorem LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j k : n) (r : R) : (singleSubSingle i k) r - (singleSubSingle i j) r = (singleSubSingle j k) r

@[simp]

theorem LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle' {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (i j k : n) (r : R) : (singleSubSingle i k) r - (singleSubSingle j k) r = (singleSubSingle i j) r

theorem LieAlgebra.SpecialLinear.sl_non_abelian (n : Type u_1) (R : Type u₂) [DecidableEq n] [CommRing R] [Fintype n] [Nontrivial R] (h : 1 < Fintype.card n) : ¬IsLieAbelian ↥(sl n R)

def LieAlgebra.Symplectic.sp (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] : LieSubalgebra R (Matrix (l ⊕ l) (l ⊕ l) R)

The symplectic Lie algebra: skew-adjoint matrices with respect to the canonical skew-symmetric bilinear form.

def LieAlgebra.Orthogonal.so (n : Type u_1) (R : Type u₂) [DecidableEq n] [CommRing R] [Fintype n] : LieSubalgebra R (Matrix n n R)

The definite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric bilinear form defined by the identity matrix.

@[simp]

theorem LieAlgebra.Orthogonal.mem_so (n : Type u_1) (R : Type u₂) [DecidableEq n] [CommRing R] [Fintype n] (A : Matrix n n R) : A ∈ so n R ↔ A.transpose = -A

def LieAlgebra.Orthogonal.indefiniteDiagonal (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] : Matrix (p ⊕ q) (p ⊕ q) R

The indefinite diagonal matrix with p 1s and q -1s.

def LieAlgebra.Orthogonal.so' (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] [Fintype p] [Fintype q] : LieSubalgebra R (Matrix (p ⊕ q) (p ⊕ q) R)

The indefinite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric bilinear form defined by the indefinite diagonal matrix.

def LieAlgebra.Orthogonal.Pso (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] (i : R) : Matrix (p ⊕ q) (p ⊕ q) R

A matrix for transforming the indefinite diagonal bilinear form into the definite one, provided the parameter i is a square root of -1.

theorem LieAlgebra.Orthogonal.pso_inv (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] [Fintype p] [Fintype q] {i : R} (hi : i * i = -1) : Pso p q R i * Pso p q R (-i) = 1

def LieAlgebra.Orthogonal.invertiblePso (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] [Fintype p] [Fintype q] {i : R} (hi : i * i = -1) : Invertible (Pso p q R i)

There is a constructive inverse of Pso p q R i.

theorem LieAlgebra.Orthogonal.indefiniteDiagonal_transform (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] [Fintype p] [Fintype q] {i : R} (hi : i * i = -1) : (Pso p q R i).transpose * indefiniteDiagonal p q R * Pso p q R i = 1

noncomputable def LieAlgebra.Orthogonal.soIndefiniteEquiv (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] [Fintype p] [Fintype q] {i : R} (hi : i * i = -1) : ↥(so' p q R) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)

An equivalence between the indefinite and definite orthogonal Lie algebras, over a ring containing a square root of -1.

theorem LieAlgebra.Orthogonal.soIndefiniteEquiv_apply (p : Type u_2) (q : Type u_3) (R : Type u₂) [DecidableEq p] [DecidableEq q] [CommRing R] [Fintype p] [Fintype q] {i : R} (hi : i * i = -1) (A : ↥(so' p q R)) : ↑((soIndefiniteEquiv p q R hi) A) = (Pso p q R i)⁻¹ * ↑A * Pso p q R i

def LieAlgebra.Orthogonal.JD (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] : Matrix (l ⊕ l) (l ⊕ l) R

A matrix defining a canonical even-rank symmetric bilinear form.

It looks like this as a 2l x 2l matrix of l x l blocks:

[ 0 1 ] [ 1 0 ]

def LieAlgebra.Orthogonal.typeD (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] : LieSubalgebra R (Matrix (l ⊕ l) (l ⊕ l) R)

The classical Lie algebra of type D as a Lie subalgebra of matrices associated to the matrix JD.

def LieAlgebra.Orthogonal.PD (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] : Matrix (l ⊕ l) (l ⊕ l) R

A matrix transforming the bilinear form defined by the matrix JD into a split-signature diagonal matrix.

It looks like this as a 2l x 2l matrix of l x l blocks:

[ 1 -1 ] [ 1 1 ]

def LieAlgebra.Orthogonal.S (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] : Matrix (l ⊕ l) (l ⊕ l) R

The split-signature diagonal matrix.

theorem LieAlgebra.Orthogonal.s_as_blocks (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] : S l R = Matrix.fromBlocks 1 0 0 (-1)

theorem LieAlgebra.Orthogonal.jd_transform (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] : (PD l R).transpose * JD l R * PD l R = 2 • S l R

theorem LieAlgebra.Orthogonal.pd_inv (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] [Invertible 2] : PD l R * ⅟2 • (PD l R).transpose = 1

instance LieAlgebra.Orthogonal.invertiblePD (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] [Invertible 2] : Invertible (PD l R)

noncomputable def LieAlgebra.Orthogonal.typeDEquivSo' (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] [Invertible 2] : ↥(typeD l R) ≃ₗ⁅R⁆ ↥(so' l l R)

An equivalence between two possible definitions of the classical Lie algebra of type D.

def LieAlgebra.Orthogonal.JB (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R

A matrix defining a canonical odd-rank symmetric bilinear form.

It looks like this as a (2l+1) x (2l+1) matrix of blocks:

[ 2 0 0 ] [ 0 0 1 ] [ 0 1 0 ]

where sizes of the blocks are:

[1 x 1 1 x l 1 x l] [l x 1 l x l l x l] [l x 1 l x l l x l]

def LieAlgebra.Orthogonal.typeB (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] : LieSubalgebra R (Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R)

The classical Lie algebra of type B as a Lie subalgebra of matrices associated to the matrix JB.

def LieAlgebra.Orthogonal.PB (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R

A matrix transforming the bilinear form defined by the matrix JB into an almost-split-signature diagonal matrix.

It looks like this as a (2l+1) x (2l+1) matrix of blocks:

[ 1 0 0 ] [ 0 1 -1 ] [ 0 1 1 ]

where sizes of the blocks are:

[1 x 1 1 x l 1 x l] [l x 1 l x l l x l] [l x 1 l x l l x l]

theorem LieAlgebra.Orthogonal.pb_inv (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] [Invertible 2] : PB l R * Matrix.fromBlocks 1 0 0 ⅟(PD l R) = 1

instance LieAlgebra.Orthogonal.invertiblePB (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] [Invertible 2] : Invertible (PB l R)

theorem LieAlgebra.Orthogonal.jb_transform (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] : (PB l R).transpose * JB l R * PB l R = 2 • Matrix.fromBlocks 1 0 0 (S l R)

theorem LieAlgebra.Orthogonal.indefiniteDiagonal_assoc (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] : indefiniteDiagonal (Unit ⊕ l) l R = (Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (Matrix.fromBlocks 1 0 0 (indefiniteDiagonal l l R))

noncomputable def LieAlgebra.Orthogonal.typeBEquivSo' (l : Type u_4) (R : Type u₂) [DecidableEq l] [CommRing R] [Fintype l] [Invertible 2] : ↥(typeB l R) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)

An equivalence between two possible definitions of the classical Lie algebra of type B.