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
lie_algebra.special_linear.sllie_algebra.symplectic.splie_algebra.orthogonal.solie_algebra.orthogonal.so'lie_algebra.orthogonal.so_indefinite_equivlie_algebra.orthogonal.type_Dlie_algebra.orthogonal.type_Blie_algebra.orthogonal.type_D_equiv_so'lie_algebra.orthogonal.type_B_equiv_so'
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 lie_equiv_matrix'.
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
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 type_D_equiv_so', so_indefinite_equiv which show the two
definitions are equivalent. Similarly for the algebras of type B.
Tags
classical lie algebra, special linear, symplectic, orthogonal
The special linear Lie algebra: square matrices of trace zero.
It is useful to define these matrices for explicit calculations in sl n R.
When j ≠ i, the elementary matrices are elements of sl n R, in fact they are part of a natural basis of sl n R.
Equations
- lie_algebra.special_linear.Eb R i j h = ⟨lie_algebra.special_linear.E R i j, _⟩
The matrix defining the canonical skew-symmetric bilinear form.
Equations
- lie_algebra.symplectic.J l R = 0.from_blocks (-1) 1 0
The symplectic Lie algebra: skew-adjoint matrices with respect to the canonical skew-symmetric bilinear form.
Equations
The definite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric bilinear form defined by the identity matrix.
Equations
The indefinite diagonal matrix with p 1s and q -1s.
Equations
- lie_algebra.orthogonal.indefinite_diagonal p q R = matrix.diagonal (sum.elim (λ (_x : p), 1) (λ (_x : q), -1))
The indefinite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric bilinear form defined by the indefinite diagonal matrix.
Equations
A matrix for transforming the indefinite diagonal bilinear form into the definite one, provided
the parameter i is a square root of -1.
Equations
- lie_algebra.orthogonal.Pso p q R i = matrix.diagonal (sum.elim (λ (_x : p), 1) (λ (_x : q), i))
An equivalence between the indefinite and definite orthogonal Lie algebras, over a ring containing a square root of -1.
Equations
- lie_algebra.orthogonal.so_indefinite_equiv p q R hi = (skew_adjoint_matrices_lie_subalgebra_equiv (lie_algebra.orthogonal.indefinite_diagonal p q R) (lie_algebra.orthogonal.Pso p q R i) _).trans (lie_algebra.equiv.of_eq (skew_adjoint_matrices_lie_subalgebra (((lie_algebra.orthogonal.Pso p q R i).transpose.mul (lie_algebra.orthogonal.indefinite_diagonal p q R)).mul (lie_algebra.orthogonal.Pso p q R i))) (lie_algebra.orthogonal.so (p ⊕ q) 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 ]
Equations
- lie_algebra.orthogonal.JD l R = 0.from_blocks 1 1 0
The classical Lie algebra of type D as a Lie subalgebra of matrices associated to the matrix
JD.
Equations
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 ]
Equations
- lie_algebra.orthogonal.PD l R = 1.from_blocks (-1) 1 1
The split-signature diagonal matrix.
Equations
An equivalence between two possible definitions of the classical Lie algebra of type D.
Equations
- lie_algebra.orthogonal.type_D_equiv_so' l R = (skew_adjoint_matrices_lie_subalgebra_equiv (lie_algebra.orthogonal.JD l R) (lie_algebra.orthogonal.PD l R) _).trans (lie_algebra.equiv.of_eq (skew_adjoint_matrices_lie_subalgebra (((lie_algebra.orthogonal.PD l R).transpose.mul (lie_algebra.orthogonal.JD l R)).mul (lie_algebra.orthogonal.PD l R))) (lie_algebra.orthogonal.so' 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]
Equations
- lie_algebra.orthogonal.JB l R = (2 • 1).from_blocks 0 0 (lie_algebra.orthogonal.JD l R)
The classical Lie algebra of type B as a Lie subalgebra of matrices associated to the matrix
JB.
Equations
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]
Equations
- lie_algebra.orthogonal.PB l R = 1.from_blocks 0 0 (lie_algebra.orthogonal.PD l R)
An equivalence between two possible definitions of the classical Lie algebra of type B.
Equations
- lie_algebra.orthogonal.type_B_equiv_so' l R = (skew_adjoint_matrices_lie_subalgebra_equiv (lie_algebra.orthogonal.JB l R) (lie_algebra.orthogonal.PB l R) _).trans ((skew_adjoint_matrices_lie_subalgebra_equiv_transpose (lie_algebra.orthogonal.indefinite_diagonal (unit ⊕ l) l R) (matrix.reindex_alg_equiv (equiv.sum_assoc punit l l)) _).trans (lie_algebra.equiv.of_eq (skew_adjoint_matrices_lie_subalgebra (⇑(matrix.reindex_alg_equiv (equiv.sum_assoc punit l l)) (lie_algebra.orthogonal.indefinite_diagonal (unit ⊕ l) l R))) (skew_adjoint_matrices_lie_subalgebra (((lie_algebra.orthogonal.PB l R).transpose.mul (lie_algebra.orthogonal.JB l R)).mul (lie_algebra.orthogonal.PB l R))) _)).symm