Lie groups and Lie algebras

Lens

MotivationH

Continuous symmetry

The rotations of space form a group: do one rotation and then another, and the result is a rotation. Unlike the symmetries of a crystal, they form a continuum — a three-dimensional manifold $SO(3)$ — and the group operations are smooth. Such Lie groups are everywhere: the rotations of a satellite, the Lorentz transformations of special relativity, the unitary groups $U(1)$ , $SU(2)$ , $SU(3)$ of the Standard Model, the symplectic groups of classical mechanics, the groups $SL(2, \R)$ and $SL(2, \Z)$ of hyperbolic geometry and number theory.

Sophus Lie's discovery, in the 1870s, was that a Lie group is almost completely determined by its infinitesimal elements — its tangent space at the identity — together with one algebraic operation, the bracket $[X, Y]$ that measures how far infinitesimal motions fail to commute. This turns hard nonlinear questions about curved groups into linear algebra. The trade is not perfect, and the lesson is partly about what is lost: the exponential map need not be onto, and different groups ( $SU(2)$ and $SO(3)$ ) can share a Lie algebra. But the gains are enormous: the representations of $SU(2)$ — the spins of quantum mechanics — come from a short algebraic argument about three matrices $e, f, h$ .

This lesson builds on smooth manifolds and on matrix groups (the matrix exponential, quaternions and $SU(2) \to SO(3)$ ). It leads to representation theory and, through root systems and dual groups, towards the Langlands programme.

IntuitionH

Infinitesimal rotations and their commutators

A rotation by a small angle $t$ about the axis $a$ moves a point $v$ by approximately $t\, a \times v$ . So the infinitesimal rotations are the maps $v \mapsto a \times v$ , given by skew-symmetric matrices $\hat a$ ; the rotation itself is recovered by "integrating", $R = \exp(t\hat a) = I + t\hat a + t^2\hat a^2/2 + \cdots$ .

Rotations do not commute, and the bracket measures the failure at second order. Rotate by a small angle about $x$ , then $y$ , then back about $x$ , then back about $y$ : you do not return home. You have rotated, approximately, by $t^2$ about the $z$ -axis. In general,

e^{tX}e^{tY}e^{-tX}e^{-tY} = I + t^2[X, Y] + O(t^3), \qquad [X, Y] = XY - YX,

and for rotations $[\hat a, \hat b] = \widehat{a \times b}$ . The vector space of infinitesimal elements, with this bracket, is the Lie algebra. Most of the group's structure is encoded in it: whether the group is commutative near the identity, which subgroups it has, how it can act linearly.

DefinitionsH

Lie groups, Lie algebras and the exponential map

Definition— Lie group

A Lie group is a group $G$ that is also a smooth manifold, such that multiplication $G \times G \to G$ and inversion $G \to G$ are smooth. A Lie group homomorphism is a smooth group homomorphism.

Definition— Lie algebra

A Lie algebra over a field $k$ is a vector space $\mathfrak g$ with a bilinear bracket $[\cdot,\cdot]$ that is alternating ( $[X, X] = 0$ ) and satisfies the Jacobi identity $[X, [Y, Z]] + [Y, [Z, X]] + [Z, [X, Y]] = 0$ . Every associative algebra is a Lie algebra under the commutator $[X, Y] = XY - YX$ ; for example $\mathfrak{gl}(n, k) = M_n(k)$ . A representation of $\mathfrak g$ on a vector space $V$ is a Lie algebra homomorphism $\mathfrak g \to \mathfrak{gl}(V)$ .

Definition— the Lie algebra of a Lie group

A vector field $X$ on $G$ is left-invariant if $d(L_g)X = X \circ L_g$ for all $g$ , where $L_g(h) = gh$ . The map $X \mapsto X_e$ identifies left-invariant vector fields with $T_eG$ , and the Lie bracket of vector fields preserves left-invariance. So $\mathfrak g = T_eG$ inherits a bracket: the Lie algebra of $G$ , of dimension $\dim G$ . A homomorphism $\varphi : G \to H$ has a differential $d\varphi_e : \mathfrak g \to \mathfrak h$ , which is a Lie algebra homomorphism.

Definition— exponential map, adjoint representation

For $X \in \mathfrak g$ the integral curve of the left-invariant field $X$ through $e$ is a one-parameter subgroup $t \mapsto \gamma_X(t)$ , $\gamma_X(s + t) = \gamma_X(s)\gamma_X(t)$ , and $\exp X = \gamma_X(1)$ . For matrix groups, $\exp X = \sum_{k \ge 0} X^k/k!$ . The adjoint representation is $\operatorname{Ad} : G \to GL(\mathfrak g)$ , the differential at $e$ of conjugation $h \mapsto ghg^{-1}$ ; for matrix groups $\operatorname{Ad}(g)X = gXg^{-1}$ , and its differential is $\operatorname{ad}(X)Y = [X, Y]$ .

For a matrix group $G \subseteq GL(n, \R)$ — a closed subgroup — all this becomes concrete: $\mathfrak g = \{X \in M_n(\R) : e^{tX} \in G \text{ for all } t\}$ with the commutator bracket (Theorem 1). Throughout the lesson, $e^X$ and $\exp X$ mean the matrix exponential.

Worked examplesH

The classical groups and their Lie algebras

Example— The classical Lie algebras

Using $\det(e^X) = e^{\operatorname{tr} X}$ and $(e^X)^{\mathsf T} = e^{X^{\mathsf T}}$ , $(e^X)^* = e^{X^*}$ :

group	Lie algebra	dimension
$GL(n, \R)$	all of $M_n(\R)$	$n^2$
$SL(n, \R)$	$\mathfrak{sl}(n, \R)$ : $\operatorname{tr} X = 0$	$n^2 - 1$
$O(n)$ , $SO(n)$	$\mathfrak{so}(n)$ : $X^{\mathsf T} = -X$	$n(n-1)/2$
$U(n)$	$\mathfrak u(n)$ : $X^* = -X$	$n^2$
$SU(n)$	$\mathfrak{su}(n)$ : $X^* = -X$ , $\operatorname{tr} X = 0$	$n^2 - 1$
$Sp(2n, \R)$	$X^{\mathsf T}J + JX = 0$	$n(2n+1)$

For instance $X \in \mathfrak{so}(n)$ gives $(e^{tX})^{\mathsf T}e^{tX} = e^{-tX}e^{tX} = I$ . Conversely, if $e^{tX}$ is orthogonal for all $t$ , differentiating $(e^{tX})^{\mathsf T}e^{tX} = I$ at $t = 0$ gives $X^{\mathsf T} + X = 0$ .

Example— so(3), su(2) and the cross product

Let $L_k = \hat e_k \in \mathfrak{so}(3)$ . Then $[L_1, L_2] = L_3$ , $[L_2, L_3] = L_1$ , $[L_3, L_1] = L_2$ : the map $a \mapsto \hat a$ is an isomorphism from $(\R^3, \times)$ to $\mathfrak{so}(3)$ . In $\mathfrak{su}(2)$ , the matrices $X_k = -\tfrac i2\sigma_k$ built from the Pauli matrices

\sigma_1 = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \quad \sigma_2 = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \quad \sigma_3 = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}

satisfy the same relations $[X_1, X_2] = X_3$ and cyclically. So $\mathfrak{su}(2) \cong \mathfrak{so}(3)$ (Lean checks both sets of relations below). Complexifying, both become $\mathfrak{sl}(2, \C)$ , with basis

e = \begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}, \quad f = \begin{pmatrix} 0 & 0 \\ 1 & 0 \end{pmatrix}, \quad h = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}, \qquad [h, e] = 2e, \; [h, f] = -2f, \; [e, f] = h .

Example— More Lie groups, and some non-examples

$\R^n$ under addition, the circle $S^1 = U(1)$ , tori $T^n = \R^n/\Z^n$ (abelian, with zero bracket); every countable discrete group (dimension $0$ ).
The Heisenberg group of upper unitriangular $3 \times 3$ real matrices; its Lie algebra has $[X, Y] = Z$ with $Z$ central — the commutation relation of position and momentum.
The group of affine maps $x \mapsto ax + b$ , $a > 0$ : two-dimensional, non-abelian, with $[X, Y] = Y$ .
The irrational line on the torus: $t \mapsto (e^{it}, e^{i\sqrt2 t}) \in T^2$ is an injective homomorphism from $\R$ whose image is dense. The image is a Lie subgroup (an immersed submanifold) that is not closed, illustrating why the Lie correspondence (Theorem 4) speaks of immersed subgroups.
Not Lie groups: the $p$ -adic integers $\Z_p$ (compact, but totally disconnected and uncountable, so not a manifold of any dimension); $\Q$ with the topology from $\R$ (not locally Euclidean). By the work of Gleason, Montgomery–Zippin and Yamabe (1952–53) on Hilbert's fifth problem, a locally compact group is a Lie group exactly when some neighbourhood of the identity contains no non-trivial subgroup.

ProofH

The Lie algebra and the exponential map

Theorem— Theorem 1 (the Lie algebra of a matrix group)

Let $G \subseteq GL(n, \R)$ be a closed subgroup and $\mathfrak g = \{X \in M_n(\R) : e^{tX} \in G \text{ for all } t \in \R\}$ . Then (a) $\mathfrak g$ is a linear subspace; (b) $gXg^{-1} \in \mathfrak g$ for $g \in G$ , $X \in \mathfrak g$ ; (c) $[X, Y] \in \mathfrak g$ for $X, Y \in \mathfrak g$ . So $\mathfrak g$ is a Lie algebra under the commutator.

Proof

(a) Clearly $\mathfrak g$ is closed under scalar multiples. For sums, use the Lie product formula $e^{X+Y} = \lim_{k\to\infty}\big(e^{X/k}e^{Y/k}\big)^k$ : indeed $e^{X/k}e^{Y/k} = I + (X + Y)/k + O(1/k^2)$ , so for large $k$ it equals $e^{(X+Y)/k + O(1/k^2)}$ (the matrix logarithm is defined near $I$ ), and its $k$ -th power is $e^{X + Y + O(1/k)}$ . Each $\big(e^{tX/k}e^{tY/k}\big)^k$ lies in $G$ , and $G$ is closed, so $e^{t(X+Y)} \in G$ .

(b) $e^{t\,gXg^{-1}} = g\, e^{tX} g^{-1} \in G$ , by applying conjugation term by term to the exponential series.

(c) By (b), the curve $c(t) = e^{tX}Ye^{-tX}$ lies in $\mathfrak g$ , a linear (hence closed) subspace of $M_n(\R)$ , so its derivative at $t = 0$ does too: $c'(0) = XY - YX$ . ∎

∎

Cartan's closed subgroup theorem says more: every closed subgroup of a Lie group is an embedded Lie subgroup, and its Lie algebra (the tangent space at $I$ ) is exactly this $\mathfrak g$ . That the commutator satisfies the Jacobi identity is a direct expansion (checked in Lean below).

Theorem— Theorem 2 (one-parameter subgroups)

If $\varphi : \R \to GL(n, \R)$ is a differentiable homomorphism, then $\varphi(t) = e^{tX}$ with $X = \varphi'(0)$ . (Every continuous homomorphism is automatically smooth; Hall, Theorem 2.14.)

Proof

From $\varphi(t + h) = \varphi(t)\varphi(h) = \varphi(h)\varphi(t)$ we get $\varphi'(t) = \varphi(t)X = X\varphi(t)$ . Let $\psi(t) = e^{-tX}\varphi(t)$ . Then $\psi'(t) = e^{-tX}\big(-X\varphi(t) + \varphi'(t)\big) = 0$ , so $\psi(t) = \psi(0) = I$ . ∎

∎

Conversely $t \mapsto e^{tX}$ is a homomorphism, because $sX$ and $tX$ commute (formalised below). The exponential map is a local diffeomorphism at $0$ ( $d\exp_0 = \mathrm{id}$ ), and:

Theorem— Theorem 3 (homomorphisms are determined by their differentials)

Let $\varphi : G \to H$ be a Lie group homomorphism. Then $\varphi(\exp X) = \exp\big(d\varphi(X)\big)$ for all $X \in \mathfrak g$ . If $G$ is connected, it is generated by $\exp(U)$ for any neighbourhood $U$ of $0$ , so $\varphi$ is determined by $d\varphi$ .

Proof

$t \mapsto \varphi(\exp tX)$ is a one-parameter subgroup of $H$ with velocity $d\varphi(X)$ at $t = 0$ , so by uniqueness of one-parameter subgroups (Theorem 2 for matrix groups; integral curves in general) it equals $t \mapsto \exp\big(t\, d\varphi(X)\big)$ . For the second claim, let $V = \exp(U)$ , a neighbourhood of $e$ , and let $G_0$ be the subgroup generated by $V$ . It is open: it contains the neighbourhood $gV$ of each of its elements $g$ . Its complement is a union of cosets $gG_0$ , each open, so $G_0$ is also closed. As $G$ is connected, $G_0 = G$ . ∎

∎

Theorem— Theorem 4 (the Lie correspondence; stated)

(a) For a Lie group $G$ with Lie algebra $\mathfrak g$ , $H \mapsto \mathfrak h$ is a bijection between connected Lie subgroups (immersed) and Lie subalgebras of $\mathfrak g$ . (b) Lie's third theorem: every finite-dimensional real Lie algebra is the Lie algebra of a simply connected Lie group $\tilde G$ , unique up to isomorphism. (c) If $\tilde G$ is simply connected, every Lie algebra homomorphism $\mathfrak g \to \mathfrak h$ is the differential of a unique homomorphism $\tilde G \to H$ . (d) The connected Lie groups with Lie algebra $\mathfrak g$ are exactly the quotients $\tilde G/\Gamma$ by discrete central subgroups $\Gamma$ .

(a) follows from the Frobenius theorem applied to the left-invariant distribution spanned by $\mathfrak h$ ; (b) from Ado's theorem (every finite-dimensional Lie algebra is a matrix Lie algebra) and (a). See Hall, Chapter 5, or Warner, Chapter 3.

ProofH

What the Lie algebra does not see

Theorem— Theorem 5 (SU(2) and SO(3))

$\mathfrak{su}(2) \cong \mathfrak{so}(3)$ , but $SU(2) \not\cong SO(3)$ . In fact $\operatorname{Ad} : SU(2) \to SO(\mathfrak{su}(2)) \cong SO(3)$ is a surjective homomorphism with kernel $\{\pm I\}$ , $SU(2)$ is diffeomorphic to $S^3$ and simply connected, and $SO(3) \cong SU(2)/\{\pm I\} \cong \R P^3$ has $\pi_1 = \Z/2$ .

Proof

The Lie algebras are isomorphic by the matching relations above. $SU(2) = \{\begin{pmatrix} \alpha & -\bar\beta \\ \beta & \bar\alpha\end{pmatrix} : |\alpha|^2 + |\beta|^2 = 1\}$ is the unit sphere $S^3 \subset \C^2$ , simply connected. $\operatorname{Ad}(g)$ preserves the inner product $\langle X, Y\rangle = -\operatorname{tr}(XY)$ on $\mathfrak{su}(2)$ , so it lies in $O(3)$ , and in $SO(3)$ since $SU(2)$ is connected. Its kernel consists of the $g$ commuting with all of $\mathfrak{su}(2)$ , hence with all of $M_2(\C)$ (which $\mathfrak{su}(2)$ spans over $\C$ ): the scalars in $SU(2)$ , namely $\pm I$ . Its differential $\operatorname{ad}$ is injective (since $\mathfrak{su}(2)$ has trivial centre), so $\operatorname{Ad}$ is a local diffeomorphism, its image is an open — hence closed — subgroup of the connected $SO(3)$ , i.e. all of it. Finally the centre of $SU(2)$ is $\{\pm I\}$ while the centre of $SO(3)$ is trivial, so the groups are not isomorphic. ∎

∎

So $SU(2)$ is the simply connected group $\tilde G$ of Theorem 4(b) for $\mathfrak{so}(3)$ , and $SO(3) = \tilde G/\{\pm I\}$ . Physically: a rotation by $2\pi$ is the identity in $SO(3)$ but $-I$ in $SU(2)$ , which is why the wave function of an electron changes sign under a full turn.

Theorem— Theorem 6 (exp is not onto SL(2, ℝ))

Every $\exp X$ with $X \in \mathfrak{sl}(2, \R)$ has trace $\ge -2$ , with equality only for $\exp X = -I$ . Consequently $A = \operatorname{diag}(-2, -\tfrac12) \in SL(2, \R)$ is not the exponential of any $X \in \mathfrak{sl}(2, \R)$ .

Proof

For a trace-zero $2 \times 2$ matrix, Cayley–Hamilton gives $X^2 = -\det(X)\, I = \delta I$ with $\delta = -\det X$ . Splitting the exponential series into even and odd powers,

e^X = \Big(\sum_{m} \frac{\delta^m}{(2m)!}\Big) I + \Big(\sum_m \frac{\delta^m}{(2m+1)!}\Big) X .

If $\delta = \mu^2 > 0$ this is $\cosh\mu\, I + \frac{\sinh\mu}{\mu}X$ , of trace $2\cosh\mu \ge 2$ . If $\delta = 0$ it is $I + X$ , of trace $2$ . If $\delta = -\theta^2 < 0$ it is $\cos\theta\, I + \frac{\sin\theta}{\theta}X$ , of trace $2\cos\theta \ge -2$ ; equality forces $\theta \in \pi + 2\pi\Z$ , so $\sin\theta = 0$ and $e^X = -I$ . Since $\operatorname{tr} A = -5/2 < -2$ , $A$ is not an exponential. ∎

∎

$A$ is nevertheless a product of two exponentials: $A = e^{\pi(f - e)}e^{(\log 2)h} = (-I)\operatorname{diag}(2, \tfrac12)$ , as Theorem 3 guarantees for the connected group $SL(2, \R)$ . On the other hand, for a compact connected Lie group the exponential map is onto: a bi-invariant Riemannian metric exists (average any inner product on $\mathfrak g$ over $\operatorname{Ad}(G)$ ), its geodesics through $e$ are the one-parameter subgroups, and the Hopf–Rinow theorem of Riemannian geometry joins $e$ to every point by a geodesic.

ProofH

Compact groups, Haar measure and complete reducibility

Theorem— Theorem 7 (Haar, 1933; stated)

Every locally compact group $G$ has a non-zero left-invariant regular Borel measure, unique up to a positive scalar. If $G$ is compact, it is finite (and also right-invariant), and can be normalised to total mass $1$ .

Theorem— Theorem 8 (complete reducibility)

Every finite-dimensional continuous representation $\rho : G \to GL(V)$ of a compact group $G$ on a real or complex vector space is a direct sum of irreducible representations.

Proof

Let $\langle\cdot,\cdot\rangle_0$ be any inner product on $V$ and $dg$ the normalised Haar measure. Define

\langle u, v\rangle = \int_G \langle \rho(g)u, \rho(g)v\rangle_0 \, dg .

It is an inner product (positivity: the integrand is positive and continuous when $u = v \ne 0$ ), and it is $G$ -invariant: $\langle\rho(h)u, \rho(h)v\rangle = \int_G \langle\rho(gh)u, \rho(gh)v\rangle_0\, dg = \langle u, v\rangle$ by right invariance of $dg$ . If $W \subseteq V$ is invariant, so is $W^\perp$ : for $u \in W^\perp$ , $w \in W$ , $\langle\rho(g)u, w\rangle = \langle u, \rho(g)^{-1}w\rangle = 0$ . Hence $V = W \oplus W^\perp$ as representations, and induction on $\dim V$ finishes the proof. ∎

∎

For finite groups the integral is the average $\frac{1}{|G|}\sum_g$ , and this is Maschke's theorem. The theorem fails for non-compact groups: the representation of $(\R, +)$ by $t \mapsto \begin{pmatrix} 1 & t \\ 0 & 1\end{pmatrix}$ has the invariant line $\R e_1$ but no invariant complement. Weyl's unitarian trick transfers complete reducibility from $SU(n)$ to $\mathfrak{sl}(n, \C)$ , whose complex representations are the same as those of $\mathfrak{su}(n)$ (complexification). The Peter–Weyl theorem goes further: the matrix coefficients of irreducible representations are dense in $L^2(G)$ , generalising Fourier series (the case $G = U(1)$ ).

ProofH

The representations of sl(2, ℂ)

For each $n \ge 0$ , let $V_n$ have basis $v_0, \dots, v_n$ and define

h v_k = (n - 2k) v_k, \qquad f v_k = v_{k+1} \;(v_{n+1} = 0), \qquad e v_k = k(n - k + 1) v_{k-1} .

Theorem— Theorem 9 (classification)

$V_n$ is an irreducible representation of $\mathfrak{sl}(2, \C)$ of dimension $n + 1$ , and every finite-dimensional irreducible complex representation of $\mathfrak{sl}(2, \C)$ is isomorphic to exactly one $V_n$ .

Proof

Key identity. In any representation (indeed in any ring with $hf - fh = -2f$ and $ef - fe = h$ ),

e f^{k+1} - f^{k+1} e = (k + 1) f^k (h - k) \qquad (k \ge 0).

For $k = 0$ it is $[e, f] = h$ . Inductively, $ef^{k+2} - f^{k+2}e = (ef^{k+1} - f^{k+1}e)f + f^{k+1}(ef - fe) = (k+1)f^k(h - k)f + f^{k+1}h$ , and $(h - k)f = f(h - k - 2)$ by $hf = f(h - 2)$ ; so it equals $f^{k+1}\big((k+1)(h - k - 2) + h\big) = (k + 2) f^{k+1}(h - k - 1)$ .

Highest weight vectors. Let $V$ be finite-dimensional and irreducible. Since $\C$ is algebraically closed, $h$ has an eigenvector $w$ , $hw = \lambda w$ . From $he = e(h + 2)$ , each $e^jw$ is either $0$ or an eigenvector with eigenvalue $\lambda + 2j$ ; these eigenvalues are distinct, and $V$ has finitely many, so for some $j$ , $v = e^jw \ne 0$ and $ev = 0$ . Write $hv = \mu v$ .

The string. Let $v_k = f^kv$ . As above, $hv_k = (\mu - 2k)v_k$ , so the non-zero $v_k$ are linearly independent; let $n$ be largest with $v_n \ne 0$ , so $v_{n+1} = 0$ . By the key identity applied to $v$ , $ev_{k+1} = (k+1)(\mu - k)v_k$ .

The weight is an integer. $0 = ev_{n+1} = (n + 1)(\mu - n)v_n$ , and $v_n \ne 0$ , so $\mu = n$ .

Irreducibility gives the rest. $\operatorname{span}(v_0, \dots, v_n)$ is non-zero and invariant under $e$ , $f$ , $h$ , so it is $V$ ; in this basis $e$ , $f$ , $h$ act by the formulas defining $V_n$ . Hence $V \cong V_n$ , and $n = \dim V - 1$ is determined by $V$ .

Existence. The formulas define a representation: $[h, e]$ and $[h, f]$ are clear, and $[e, f]v_k = (k+1)(n - k)v_k - k(n - k + 1)v_k = (n - 2k)v_k = hv_k$ . It is irreducible: an invariant subspace contains an eigenvector of $h$ , i.e. some $v_k$ ; applying $e$ repeatedly gives $v_0$ (the coefficients $k(n - k + 1)$ are non-zero for $1 \le k \le n$ ), and applying $f$ gives all $v_k$ . ∎

∎

Concretely, $V_n \cong \operatorname{Sym}^n(\C^2)$ , the homogeneous polynomials of degree $n$ in $x, y$ , with $e = x\partial_y$ , $f = y\partial_x$ , $h = x\partial_x - y\partial_y$ ; $V_1 = \C^2$ is the defining representation and $V_2 \cong \mathfrak{sl}(2, \C)$ is the adjoint representation. The Casimir element $C = ef + fe + \tfrac12h^2$ commutes with $\mathfrak{sl}(2)$ and acts on $V_n$ by $n(n+2)/2$ . Since $SU(2)$ is simply connected, every $V_n$ integrates to a representation of $SU(2)$ (Theorem 4(c)); it descends to $SO(3)$ exactly when $-I$ acts trivially, i.e. when $n$ is even. In physics $V_n$ is the spin- $n/2$ representation; the "half-integer spins" are the representations of $SU(2)$ that are not representations of $SO(3)$ .

Tensor products decompose by Clebsch–Gordan: the weights of $V_m \otimes V_n$ are the sums of weights, and peeling off highest weights gives

V_m \otimes V_n \cong V_{m+n} \oplus V_{m+n-2} \oplus \cdots \oplus V_{|m-n|} .

Worked examplesH

A first look at root systems: sl(3, ℂ)

Example— The roots of sl(3, ℂ)

Let $\mathfrak h \subset \mathfrak{sl}(3, \C)$ be the diagonal trace-zero matrices $H = \operatorname{diag}(h_1, h_2, h_3)$ , a maximal abelian subalgebra of semisimple elements (a Cartan subalgebra). The elementary matrices $E_{ij}$ ( $i \ne j$ ) are simultaneous eigenvectors of $\operatorname{ad}(H)$ :

[H, E_{ij}] = (h_i - h_j)E_{ij} .

So $\mathfrak{sl}(3, \C) = \mathfrak h \oplus \bigoplus_{i \ne j}\C E_{ij}$ (dimensions $2 + 6 = 8$ ), and the six linear functionals $\alpha_{ij} = \varepsilon_i - \varepsilon_j$ on $\mathfrak h$ are the roots. In the plane $\{x_1 + x_2 + x_3 = 0\}$ they form a regular hexagon, all of the same length; the simple roots $\alpha_1 = \varepsilon_1 - \varepsilon_2$ , $\alpha_2 = \varepsilon_2 - \varepsilon_3$ make an angle of $120^\circ$ , every root is $\pm\alpha_1$ , $\pm\alpha_2$ or $\pm(\alpha_1 + \alpha_2)$ , and the Cartan matrix $\big(2(\alpha_i, \alpha_j)/(\alpha_j, \alpha_j)\big)$ is $\begin{pmatrix} 2 & -1 \\ -1 & 2\end{pmatrix}$ . The Weyl group, generated by the reflections in the roots, is $S_3$ permuting the coordinates.

The root system $A_2$ of $\mathfrak{sl}(3, \C)$: six roots $\varepsilon_i - \varepsilon_j$ forming a regular hexagon. The simple roots $\alpha_1$ and $\alpha_2$ are drawn in gold; their sum $\alpha_1 + \alpha_2 = \varepsilon_1 - \varepsilon_3$ lies between them.

Each pair $\pm\alpha$ gives an $\mathfrak{sl}(2)$ -triple ( $E_{ij}$ , $E_{ji}$ , $E_{ii} - E_{jj}$ ), so every representation of $\mathfrak{sl}(3)$ restricts to representations of three copies of $\mathfrak{sl}(2)$ — and Theorem 9 forces the weights to be integral on the coroots. This is the start of the general theory: Killing (1888–90) and Cartan (1894) classified the complex simple Lie algebras by their root systems — the four infinite families $A_n$ ( $\mathfrak{sl}(n+1)$ ), $B_n$ ( $\mathfrak{so}(2n+1)$ ), $C_n$ ( $\mathfrak{sp}(2n)$ ), $D_n$ ( $\mathfrak{so}(2n)$ ) and five exceptional algebras $E_6, E_7, E_8, F_4, G_2$ — and the irreducible representations by their highest weights (Cartan, Weyl).

Formal mathematicsF

Lie groups in Lean and Mathlib

Mathlib defines a Lie group as a group with a manifold structure for which multiplication and inversion are smooth, and provides the basic examples. We cite two: the units of a complete normed algebra (such as $GL(n, \R)$ ) and the circle.

units_lie_groupLean 4Applies a library theoremFormally verified

/-- **`GL` is a Lie group.** The group of units `Rˣ` of a complete normed algebra `R` is a Lie
group, modelled on `R` itself (it is an open subset of `R`). For `R = Mₙ(ℝ)` with an operator
norm, this is `GL(n, ℝ)`. Mathlib's instance from `UnitsOfNormedAlgebra`. -/
theorem units_lie_group {𝕜 : Type*} [NontriviallyNormedField 𝕜] {R : Type*} [NormedRing R]
    [CompleteSpace R] [NormedAlgebra 𝕜 R] (n : WithTop ℕ∞) :
    LieGroup (modelWithCornersSelf 𝕜 R) n Rˣ :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

circle_lie_groupLean 4Applies a library theoremFormally verified

/-- **The circle group `U(1)` is a Lie group** (indeed analytic, `ω`), with the charts of the
`1`-sphere. Mathlib's instance in `Instances.Sphere`. -/
theorem circle_lie_group : LieGroup (𝓡 1) ω Circle :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

Mathlib also equips the tangent space at the identity of any Lie group with the bracket of left-invariant vector fields (GroupLieAlgebra, an instance of LieAlgebra), exactly as in our definition. On the algebraic side, the commutator makes every associative ring a Lie ring; the Jacobi identity is an expansion of twelve products, which we prove directly and also cite in Mathlib's form:

commutator_jacobiLean 4Proved here from basic factsFormally verified

/-- **The commutator satisfies the Jacobi identity.** In any associative ring, with
`[X, Y] = XY - YX`: `[X, [Y, Z]] + [Y, [Z, X]] + [Z, [X, Y]] = 0` — expand the twelve products and
they cancel in pairs. So every associative algebra, in particular `Mₙ(ℝ)`, is a Lie algebra. -/
theorem commutator_jacobi {A : Type*} [Ring A] (X Y Z : A) :
    X * (Y * Z - Z * Y) - (Y * Z - Z * Y) * X + (Y * (Z * X - X * Z) - (Z * X - X * Z) * Y) +
      (Z * (X * Y - Y * X) - (X * Y - Y * X) * Z) = 0 := by
  noncomm_ring

Axioms used: propext, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

lie_jacobi_libraryLean 4Applies a library theoremFormally verified

/-- The same identity for Mathlib's Lie bracket on a ring (`⁅X, Y⁆ = XY - YX`, `Ring.lie_def`):
Mathlib's `lie_jacobi`, valid in every Lie ring. -/
theorem lie_jacobi_library {A : Type*} [Ring A] (X Y Z : A) :
    ⁅X, ⁅Y, Z⁆⁆ + ⁅Y, ⁅Z, X⁆⁆ + ⁅Z, ⁅X, Y⁆⁆ = 0 :=
  lie_jacobi X Y Z

Axioms used: propext, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

The matrix exponential is NormedSpace.exp. Two independent results from Theorems 1 and 2: $t \mapsto e^{tX}$ is a one-parameter subgroup, and the exponential of a skew-symmetric matrix is orthogonal:

exp_one_parameterLean 4Proved here from basic factsFormally verified

/-- **`t ↦ exp(tX)` is a one-parameter subgroup**: `exp((s + t)X) = exp(sX) exp(tX)`. The two
exponents commute (both are multiples of `X`), so Mathlib's `Matrix.exp_add_of_commute` applies. -/
theorem exp_one_parameter (X : Matrix n n ℝ) (s t : ℝ) :
    NormedSpace.exp ((s + t) • X) = NormedSpace.exp (s • X) * NormedSpace.exp (t • X) := by
  rw [add_smul]
  exact Matrix.exp_add_of_commute _ _ (((Commute.refl X).smul_left s).smul_right t)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

exp_skew_orthogonalLean 4Proved here from basic factsFormally verified

/-- **The exponential of a skew-symmetric matrix is orthogonal**: if `Aᵀ = -A` then
`(exp A)ᵀ exp A = exp(Aᵀ) exp(A) = exp(-A) exp(A) = exp(0) = I`. So `exp` maps `so(n)` into
`O(n)` (indeed into `SO(n)`, by connectedness). -/
theorem exp_skew_orthogonal {A : Matrix n n ℝ} (hA : Aᵀ = -A) :
    (NormedSpace.exp A)ᵀ * NormedSpace.exp A = 1 := by
  rw [← Matrix.exp_transpose, hA,
    ← Matrix.exp_add_of_commute _ _ ((Commute.refl A).neg_left), neg_add_cancel,
    NormedSpace.exp_zero]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

Theorem 5's Lie algebra half: $\mathfrak{so}(3)$ is $\R^3$ with the cross product, and the basis $X_k = -\frac i2\sigma_k$ of $\mathfrak{su}(2)$ has the same structure constants. The group half begins with $-I$ , a non-trivial central element of $SU(2)$ :

hatLean 4Formally verified

/-- The **hat map** `ℝ³ → so(3)`: `â` is the skew-symmetric matrix with `â v = a × v`. -/
def hat (a : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ :=
  !![0, -a 2, a 1; a 2, 0, -a 0; -a 1, a 0, 0]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

hat_bracketLean 4Proved here from basic factsFormally verified

/-- **`so(3)` is `ℝ³` with the cross product**: `[â, b̂] = (a × b)^`. With the basis
`Lᵢ = êᵢ` this reads `[L₁, L₂] = L₃`, `[L₂, L₃] = L₁`, `[L₃, L₁] = L₂`. -/
theorem hat_bracket (a b : Fin 3 → ℝ) :
    hat a * hat b - hat b * hat a = hat (crossProduct a b) := by
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [hat, cross_apply] <;> ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

su2BasisLean 4Formally verified

/-- A basis of `su(2)`, the trace-zero skew-Hermitian `2 × 2` matrices: `Xₖ = -(i/2) σₖ` for the
Pauli matrices `σ₁, σ₂, σ₃`. -/
noncomputable def su2Basis : Fin 3 → Matrix (Fin 2) (Fin 2) ℂ :=
  ![!![0, -Complex.I / 2; -Complex.I / 2, 0],
    !![0, -1 / 2; 1 / 2, 0],
    !![-Complex.I / 2, 0; 0, Complex.I / 2]]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

su2_bracketsLean 4Proved here from basic factsFormally verified

/-- **`su(2)` has the same structure constants as `so(3)`**: `[X₁, X₂] = X₃`, `[X₂, X₃] = X₁`,
`[X₃, X₁] = X₂`. Hence `Xₖ ↦ Lₖ` is a Lie algebra isomorphism `su(2) ≅ so(3)`, although the
groups `SU(2)` and `SO(3)` are not isomorphic. -/
theorem su2_brackets :
    su2Basis 0 * su2Basis 1 - su2Basis 1 * su2Basis 0 = su2Basis 2 ∧
      su2Basis 1 * su2Basis 2 - su2Basis 2 * su2Basis 1 = su2Basis 0 ∧
      su2Basis 2 * su2Basis 0 - su2Basis 0 * su2Basis 2 = su2Basis 1 := by
  refine ⟨?_, ?_, ?_⟩ <;>
  · ext i j
    fin_cases i <;> fin_cases j <;>
      simp [su2Basis] <;> ring_nf <;>
      simp [Complex.ext_iff] <;> norm_num

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

neg_one_mem_su2Lean 4Proved here from basic factsFormally verified

/-- `-I` lies in `SU(2)` (it is unitary with determinant `(-1)² = 1`) and is central but not the
identity; so the centre of `SU(2)` is non-trivial, whereas that of `SO(3)` is trivial — one way to
see that the two groups are not isomorphic. -/
theorem neg_one_mem_su2 :
    (-1 : Matrix (Fin 2) (Fin 2) ℂ) ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ ∧
      (-1 : Matrix (Fin 2) (Fin 2) ℂ) ≠ 1 := by
  refine ⟨?_, ?_⟩
  · rw [Matrix.mem_specialUnitaryGroup_iff, Matrix.mem_unitaryGroup_iff]
    simp [Matrix.det_neg]
  · intro h
    have := congrFun (congrFun h 0) 0
    norm_num at this

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

The matrices $e, f, h$ form an $\mathfrak{sl}_2$ -triple in Mathlib's sense:

sl2ELean 4Formally verified

/-- The standard basis of `sl(2)`: `e = [[0, 1], [0, 0]]`. -/
def sl2E : Matrix (Fin 2) (Fin 2) ℚ := !![0, 1; 0, 0]

Axioms used: propext, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

sl2FLean 4Formally verified

/-- `f = [[0, 0], [1, 0]]`. -/
def sl2F : Matrix (Fin 2) (Fin 2) ℚ := !![0, 0; 1, 0]

Axioms used: propext, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

sl2HLean 4Formally verified

/-- `h = [[1, 0], [0, -1]]`. -/
def sl2H : Matrix (Fin 2) (Fin 2) ℚ := !![1, 0; 0, -1]

Axioms used: propext, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

sl2_tripleLean 4Proved here from basic factsFormally verified

/-- **The relations of `sl(2)`**: `[h, e] = 2e`, `[h, f] = -2f`, `[e, f] = h`. In Mathlib's language,
`(h, e, f)` is an `sl₂`-triple in the Lie algebra of `2 × 2` matrices. -/
theorem sl2_triple : IsSl2Triple sl2H sl2E sl2F where
  h_ne_zero := by
    intro h
    have := congrFun (congrFun h 0) 0
    simp [sl2H] at this
  lie_e_f := by
    rw [Ring.lie_def]
    ext i j
    fin_cases i <;> fin_cases j <;> simp [sl2E, sl2F, sl2H]
  lie_h_e_nsmul := by
    rw [Ring.lie_def]
    ext i j
    fin_cases i <;> fin_cases j <;> norm_num [sl2E, sl2H]
  lie_h_f_nsmul := by
    rw [Ring.lie_def]
    ext i j
    fin_cases i <;> fin_cases j <;> norm_num [sl2F, sl2H]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

The heart of Theorem 9 — the key identity, proved by induction in an arbitrary ring, and the step "the highest weight is the length of the string" for operators on a complex vector space — and Mathlib's own, more general version for finite-dimensional representations:

e_f_powLean 4Proved here from basic factsFormally verified

/-- **The key identity for `sl(2)`-representations.** In any ring (for instance the operators on a
representation) in which `hf - fh = -2f` and `ef - fe = h`,
`e fᵏ⁺¹ - fᵏ⁺¹ e = (k + 1) fᵏ (h - k)`. Induction on `k`: commute `e` past one `f` at a time, and
use `(h - k) f = f (h - k - 2)`. -/
theorem e_f_pow {A : Type*} [Ring A] {e f h : A} (hhf : h * f - f * h = -2 * f)
    (hef : e * f - f * e = h) (k : ℕ) :
    e * f ^ (k + 1) - f ^ (k + 1) * e = ((k : A) + 1) * f ^ k * (h - k) := by
  have hcomm : ∀ m : ℕ, (m : A) * f = f * m := fun m => (Nat.cast_commute m f)
  have h2 : (2 : A) * f = f * 2 := by
    rw [show (2 : A) = ((2 : ℕ) : A) by norm_num]
    exact hcomm 2
  have h1 : h * f = f * h + -2 * f := by rw [← hhf]; abel
  have hshift : ∀ m : ℕ, (h - m) * f = f * (h - m - 2) := by
    intro m
    calc (h - m) * f = h * f - m * f := sub_mul _ _ _
      _ = (f * h + -2 * f) - f * m := by rw [h1, hcomm]
      _ = f * (h - m - 2) := by rw [neg_mul, h2]; noncomm_ring
  induction k with
  | zero => simpa using hef
  | succ k ih =>
    calc e * f ^ (k + 1 + 1) - f ^ (k + 1 + 1) * e
        = (e * f ^ (k + 1) - f ^ (k + 1) * e) * f + f ^ (k + 1) * (e * f - f * e) := by
          rw [pow_succ f (k + 1)]
          noncomm_ring
      _ = ((k : A) + 1) * f ^ k * ((h - k) * f) + f ^ (k + 1) * h := by
          rw [ih, hef]
          noncomm_ring
      _ = ((k : A) + 1) * (f ^ k * f) * (h - k - 2) + f ^ (k + 1) * h := by
          rw [hshift k]
          noncomm_ring
      _ = f ^ (k + 1) * (((k : A) + 1) * (h - k - 2) + h) := by
          rw [← pow_succ]
          have hc : ((k : A) + 1) * f ^ (k + 1) = f ^ (k + 1) * ((k : A) + 1) :=
            ((Nat.cast_commute k _).add_left (Commute.one_left _))
          rw [mul_add, ← mul_assoc, hc, mul_assoc]
      _ = (((k + 1 : ℕ) : A) + 1) * f ^ (k + 1) * (h - ((k + 1 : ℕ) : A)) := by
          have hc : (((k + 1 : ℕ) : A) + 1) * f ^ (k + 1) =
              f ^ (k + 1) * (((k + 1 : ℕ) : A) + 1) :=
            ((Nat.cast_commute (k + 1) _).add_left (Commute.one_left _))
          rw [hc, mul_assoc]
          congr 1
          push_cast
          noncomm_ring

Axioms used: propext, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

highest_weight_natLean 4Proved here from basic factsFormally verified

/-- **Highest weights are natural numbers.** Let `E, F, H` act on a complex vector space with the
`sl(2)` relations, and let `v` be a highest weight vector: `E v = 0`, `H v = λ v`. If the string
`v, Fv, F²v, …` stops after `Fⁿ v ≠ 0` (that is, `Fⁿ⁺¹ v = 0`), then `λ = n`. Apply `e_f_pow` to
`v`: `0 = E Fⁿ⁺¹ v - Fⁿ⁺¹ E v = (n + 1)(λ - n) Fⁿ v`. -/
theorem highest_weight_nat {M : Type*} [AddCommGroup M] [Module ℂ M]
    {E F H : Module.End ℂ M} (hhf : H * F - F * H = -2 * F) (hef : E * F - F * E = H)
    {v : M} {μ : ℂ} (hE : E v = 0) (hH : H v = μ • v) {n : ℕ}
    (hn : (F ^ n) v ≠ 0) (hn1 : (F ^ (n + 1)) v = 0) : μ = n := by
  have key := LinearMap.congr_fun (e_f_pow hhf hef n) v
  have hl : (E * F ^ (n + 1) - F ^ (n + 1) * E) v = 0 := by
    rw [LinearMap.sub_apply, Module.End.mul_apply, Module.End.mul_apply, hn1, hE, map_zero,
      map_zero, sub_zero]
  have hv : (H - (n : Module.End ℂ M)) v = (μ - n) • v := by
    rw [LinearMap.sub_apply, hH, Module.End.natCast_apply, sub_smul, Nat.cast_smul_eq_nsmul]
  have hr : (((n : Module.End ℂ M) + 1) * F ^ n * (H - n)) v =
      (((n : ℂ) + 1) * (μ - n)) • (F ^ n) v := by
    rw [Module.End.mul_apply, Module.End.mul_apply, hv, map_smul, LinearMap.add_apply,
      Module.End.natCast_apply, Module.End.one_apply, ← Nat.cast_smul_eq_nsmul ℂ, smul_smul,
      ← add_smul]
    congr 1
    ring
  rw [hl, hr] at key
  have hscalar : ((n : ℂ) + 1) * (μ - n) = 0 := by
    by_contra hne
    exact hn (smul_eq_zero.mp key.symm |>.resolve_left hne)
  rcases mul_eq_zero.mp hscalar with h | h
  · exfalso
    have : ((n + 1 : ℕ) : ℂ) = 0 := by push_cast; exact h
    exact Nat.succ_ne_zero n (Nat.cast_eq_zero.mp this)
  · exact sub_eq_zero.mp h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

primitive_vector_natLean 4Applies a library theoremFormally verified

/-- Mathlib's version, for any finite-dimensional (Noetherian, torsion-free) representation of a
Lie algebra over a field of characteristic `0` with an `sl₂`-triple: the eigenvalue of a primitive
vector is a natural number. Mathlib's `IsSl2Triple.HasPrimitiveVectorWith.exists_nat`. -/
theorem primitive_vector_nat {K L M : Type*} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L]
    [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M]
    [IsNoetherian K M] [Module.IsTorsionFree K M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {μ : K}
    (P : t.HasPrimitiveVectorWith m μ) : ∃ n : ℕ, μ = n :=
  P.exists_nat

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

The algebraic core of Theorem 6, Cayley–Hamilton on $\mathfrak{sl}(2)$ :

sl2_sq_scalarLean 4Proved here from basic factsFormally verified

/-- **On `sl(2)`, `X² = -det(X) I`** (Cayley–Hamilton for trace-zero `2 × 2` matrices). This is
the algebraic core of the computation `exp X = cosh(√δ) I + (sinh √δ / √δ) X` with `δ = -det X`,
which shows `tr(exp X) ≥ -2` for `X ∈ sl(2, ℝ)`, so that `diag(-2, -1/2) ∈ SL(2, ℝ)` is not an
exponential. -/
theorem sl2_sq_scalar {X : Matrix (Fin 2) (Fin 2) ℝ} (hX : X.trace = 0) :
    X * X = -X.det • (1 : Matrix (Fin 2) (Fin 2) ℝ) := by
  rw [Matrix.trace_fin_two] at hX
  have hd : X 1 1 = -X 0 0 := by linarith
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [Matrix.mul_apply, Fin.sum_univ_two, Matrix.det_fin_two, hd] <;> ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

And the existence of Haar measure, with its finiteness on compact groups, from Mathlib's measure theory (Theorem 7):

haar_measureLean 4Applies a library theoremFormally verified

/-- **Haar measure exists.** Every locally compact topological group carries a left-invariant
Haar measure (finite on compact sets, positive on open sets). For a compact group it is finite,
and averaging an inner product against it produces an invariant one — the key to complete
reducibility. Mathlib's `MeasureTheory.Measure.haar` and its `IsHaarMeasure` instance. -/
theorem haar_measure {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    (MeasureTheory.Measure.haar : MeasureTheory.Measure G).IsHaarMeasure :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

haar_finite_compactLean 4Applies a library theoremFormally verified

/-- On a **compact** group the Haar measure is finite, so it can be normalised to a probability
measure and used to average. A Mathlib instance (compact sets have finite Haar measure). -/
theorem haar_finite_compact {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.haar : MeasureTheory.Measure G) :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LieGroups.leanTry it in the Lean web editor

What is and is not formalised. Proved here: the Jacobi identity for commutators, the one-parameter subgroup property, $\exp(\mathfrak{so}(n)) \subseteq O(n)$ , the brackets of $\mathfrak{so}(3)$ and $\mathfrak{su}(2)$ , $-I \in SU(2)$ , the $\mathfrak{sl}_2$ relations, the key identity and the integrality of highest weights (the decisive steps of Theorem 9), and $X^2 = -\det(X) I$ on $\mathfrak{sl}(2)$ . Cited from Mathlib: the Lie group structures on $GL$ and $S^1$ , the Jacobi identity in Lie rings, Mathlib's theorem on primitive vectors, and Haar measure. Not formalised: Theorems 1 and 4 in general, the isomorphism $SU(2)/\{\pm I\} \cong SO(3)$ and the triviality of the centre of $SO(3)$ , the series computation and conclusion of Theorem 6, Theorem 8 (Mathlib lacks the integral of a representation against Haar measure in this form), and root systems (Mathlib has a theory of root pairings, not used here). Mathlib lists $\det(e^X) = e^{\operatorname{tr} X}$ as future work.

ComputationC

Exponentials and representations, computed

The first program computes matrix exponentials by scaling and squaring: the exponential of a skew-symmetric matrix is a rotation matching Rodrigues' formula; $\det e^X = e^{\operatorname{tr}X}$ ; the group commutator $e^{tX}e^{tY}e^{-tX}e^{-tY}$ differs from $I + t^2[X, Y]$ by $O(t^3)$ ; and thousands of random elements of $\exp(\mathfrak{sl}(2, \R))$ never have trace below $-2$ .

The matrix exponential: rotations, commutators and SL(2, R)PythonNumerical approximationExperimental evidenceComputationally tested

"""The matrix exponential: rotations, determinants, commutators and SL(2, R).

1. exp of a skew-symmetric 3 x 3 matrix is a rotation (orthogonal, det 1),
   agrees with Rodrigues' formula and fixes the axis.
2. det(exp X) = e^(tr X), checked on random 4 x 4 matrices.
3. The group commutator exp(tX) exp(tY) exp(-tX) exp(-tY) equals
   I + t^2 [X, Y] up to an error of order t^3: the Lie bracket measures how
   far the flows fail to commute.
4. In SL(2, R) every exponential exp(X) (X of trace 0) has trace >= -2, so
   diag(-2, -1/2), of trace -5/2, is not an exponential.
The exponential is computed by scaling and squaring a Taylor series.
"""

import math

import numpy as np

def expm(a, terms=20):
    """Matrix exponential by scaling, a Taylor polynomial, and squaring."""
    a = np.asarray(a, dtype=float)
    norm = np.linalg.norm(a, 1)
    s = max(0, int(math.ceil(math.log2(norm))) + 1) if norm > 0 else 0
    b = a / 2**s
    result = np.eye(len(a))
    term = np.eye(len(a))
    for k in range(1, terms):
        term = term @ b / k
        result = result + term
    for _ in range(s):
        result = result @ result
    return result

def hat(v):
    """The skew-symmetric matrix of the cross product with v."""
    x, y, z = v
    return np.array([[0.0, -z, y], [z, 0.0, -x], [-y, x, 0.0]])

def rodrigues(v):
    """Rotation by angle |v| about the axis v: I + sin(t)/t K + (1-cos t)/t^2 K^2."""
    t = np.linalg.norm(v)
    k = hat(v)
    return np.eye(3) + math.sin(t) / t * k + (1 - math.cos(t)) / t**2 * k @ k

def group_commutator_error(x, y, t):
    """|| exp(tX) exp(tY) exp(-tX) exp(-tY) - I - t^2 [X, Y] || (max norm)."""
    g = expm(t * x) @ expm(t * y) @ expm(-t * x) @ expm(-t * y)
    return np.abs(g - np.eye(len(x)) - t**2 * (x @ y - y @ x)).max()

def min_trace_of_sl2_exponentials(samples, scale, seed=2024):
    """Smallest trace of exp(X) over random trace-zero 2 x 2 matrices X."""
    rng = np.random.default_rng(seed)
    best = math.inf
    for _ in range(samples):
        a, b, c = rng.normal(0, scale, 3)
        best = min(best, np.trace(expm([[a, b], [c, -a]])))
    return best

def main():
    v = np.array([0.3, -1.2, 0.8])
    r = expm(hat(v))
    print("1. exp of a skew-symmetric matrix (axis v = (0.3, -1.2, 0.8))")
    print(f"   |R^T R - I| = {np.abs(r.T @ r - np.eye(3)).max():.1e},"
          f"  det R = {np.linalg.det(r):.12f}")
    print(f"   |R - Rodrigues| = {np.abs(r - rodrigues(v)).max():.1e},"
          f"  |R v - v| = {np.abs(r @ v - v).max():.1e}")
    rng = np.random.default_rng(7)
    worst = 0.0
    for _ in range(5):
        x = rng.normal(0, 0.7, (4, 4))
        lhs, rhs = np.linalg.det(expm(x)), math.exp(np.trace(x))
        worst = max(worst, abs(lhs - rhs) / rhs)
    print(f"2. det(exp X) = e^(tr X): largest relative error {worst:.1e}"
          " (5 random X)")
    x = np.array([[0.0, 1.0], [0.0, 0.0]])
    y = np.array([[0.0, 0.0], [1.0, 0.0]])
    print("3. Group commutator of e = [[0,1],[0,0]], f = [[0,0],[1,0]]:")
    for t in [0.1, 0.01, 0.001]:
        err = group_commutator_error(x, y, t)
        print(f"   t = {t:<6} error = {err:.2e}   error / t^3 = {err / t**3:.3f}")
    m = min_trace_of_sl2_exponentials(3000, 2.0)
    print("4. SL(2, R): smallest trace of exp(X) over 3000 random X in sl(2, R):")
    print(f"   {m:.6f} (never below -2)")
    rot = expm([[0.0, -math.pi], [math.pi, 0.0]])
    print(f"   exp([[0, -pi], [pi, 0]]) has trace {np.trace(rot):.6f} (it is -I)")
    print("   diag(-2, -1/2) has det 1 and trace -2.5 < -2: not an exponential.")
    print()
    print("Epistemic status: floating-point computation and random sampling.")
    print("Part 4 is evidence, not proof, that tr exp(X) >= -2 on sl(2, R); the")
    print("lesson proves it from X^2 = -det(X) I. Parts 1-3 illustrate theorems")
    print("proved in the lesson (orthogonality in part 1 also in Lean).")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

For $e$ and $f$ the ratio error $/t^3$ is $1.000$ at every scale, so the commutator really is a second-order effect with a definite third-order correction. Part 4 is sampling: it cannot prove Theorem 6, but it would quickly reveal a counterexample if the theorem were false.

The second program builds the representations $V_n$ with exact integers, checks the relations and the Casimir, decomposes tensor products by peeling off highest weights, and computes the roots of $\mathfrak{sl}(3)$ as eigenvalues of $\operatorname{ad}(H)$ .

Representations of sl(2) and the roots of sl(3)PythonExact computationExhaustive finite checkComputationally tested

"""The irreducible representations of sl(2, C), and the roots of sl(3, C).

For each n, the (n+1)-dimensional representation V_n has a basis
v_0, ..., v_n with  h v_k = (n - 2k) v_k,  f v_k = v_(k+1),
e v_k = k (n - k + 1) v_(k-1). We build these matrices with exact integers,
check the relations [h, e] = 2e, [h, f] = -2f, [e, f] = h, compute the
Casimir element ef + fe + h^2/2 (a scalar, n(n+2)/2, by Schur's lemma) and
decompose tensor products by peeling off highest weights (Clebsch-Gordan).
Finally it computes the eigenvalues of ad(H) on sl(3) for diagonal H: the six
roots, which form a regular hexagon (the root system A2). All exact.
"""

import itertools
import math
from fractions import Fraction

def zeros(d):
    """A d x d zero matrix (lists of Fractions)."""
    return [[Fraction(0)] * d for _ in range(d)]

def mat_mul(a, b):
    """Product of square matrices given as lists of lists."""
    d = len(a)
    return [[sum(a[i][k] * b[k][j] for k in range(d)) for j in range(d)]
            for i in range(d)]

def bracket(a, b):
    """The commutator ab - ba."""
    ab, ba = mat_mul(a, b), mat_mul(b, a)
    return [[x - y for x, y in zip(r, s)] for r, s in zip(ab, ba)]

def scale(c, a):
    """The matrix c * a."""
    return [[c * x for x in row] for row in a]

def irrep(n):
    """Matrices (e, f, h) of V_n in the basis v_0, ..., v_n (column k = image of v_k)."""
    d = n + 1
    e, f, h = zeros(d), zeros(d), zeros(d)
    for k in range(d):
        h[k][k] = Fraction(n - 2 * k)
        if k + 1 < d:
            f[k + 1][k] = Fraction(1)
        if k >= 1:
            e[k - 1][k] = Fraction(k * (n - k + 1))
    return e, f, h

def relations_hold(n):
    """Check [h, e] = 2e, [h, f] = -2f, [e, f] = h in V_n."""
    e, f, h = irrep(n)
    return (bracket(h, e) == scale(2, e) and bracket(h, f) == scale(-2, f)
            and bracket(e, f) == h)

def casimir(n):
    """The matrix ef + fe + h^2 / 2 on V_n."""
    e, f, h = irrep(n)
    ef, fe, hh = mat_mul(e, f), mat_mul(f, e), mat_mul(h, h)
    return [[ef[i][j] + fe[i][j] + hh[i][j] / 2 for j in range(n + 1)]
            for i in range(n + 1)]

def decompose(weights):
    """Split a multiset of h-weights into irreducibles: list of highest weights."""
    remaining = sorted(weights, reverse=True)
    parts = []
    while remaining:
        top = remaining[0]
        parts.append(top)
        for w in range(top, -top - 1, -2):
            remaining.remove(w)
    return parts

def tensor_weights(m, n):
    """Weights of V_m (x) V_n: all sums of a weight of V_m and one of V_n."""
    return [a + b for a in range(-m, m + 1, 2) for b in range(-n, n + 1, 2)]

def sl3_roots():
    """Roots of sl(3): ad(H) E_ij = (h_i - h_j) E_ij; return the pairs (i, j)."""
    return [(i, j) for i, j in itertools.permutations(range(3), 2)]

def ad_check(diag):
    """Verify [H, E_ij] = (h_i - h_j) E_ij with matrices, for H = diag(diag)."""
    hmat = zeros(3)
    for k in range(3):
        hmat[k][k] = Fraction(diag[k])
    for i, j in sl3_roots():
        eij = zeros(3)
        eij[i][j] = Fraction(1)
        if bracket(hmat, eij) != scale(Fraction(diag[i] - diag[j]), eij):
            return False
    return True

def root_vector(i, j):
    """The root e_i - e_j, in an orthonormal basis of the plane x + y + z = 0."""
    v = [0.0, 0.0, 0.0]
    v[i], v[j] = 1.0, -1.0
    u1 = (1 / math.sqrt(2), -1 / math.sqrt(2), 0.0)
    u2 = (1 / math.sqrt(6), 1 / math.sqrt(6), -2 / math.sqrt(6))
    return (sum(a * b for a, b in zip(v, u1)), sum(a * b for a, b in zip(v, u2)))

def cartan_matrix(simple):
    """Cartan integers 2 (a, b) / (b, b) for simple roots given as 2D vectors."""
    def dot(a, b):
        return a[0] * b[0] + a[1] * b[1]
    return [[round(2 * dot(a, b) / dot(b, b)) for b in simple] for a in simple]

def main():
    ok = all(relations_hold(n) for n in range(9))
    print(f"1. V_n for n = 0..8: [h,e] = 2e, [h,f] = -2f, [e,f] = h hold: {ok}")
    for n in range(5):
        c = casimir(n)
        scalar = all(c[i][j] == (c[0][0] if i == j else 0)
                     for i in range(n + 1) for j in range(n + 1))
        weights = " ".join(str(n - 2 * k) for k in range(n + 1))
        print(f"   V_{n}: weights {weights:<14} Casimir = {c[0][0]}"
              f" (scalar: {scalar})")
    print("2. Clebsch-Gordan, by peeling off highest weights:")
    for m, n in [(1, 1), (2, 1), (2, 2), (3, 2)]:
        parts = " + ".join(f"V_{p}" for p in decompose(tensor_weights(m, n)))
        print(f"   V_{m} (x) V_{n} = {parts}")
    print("3. Roots of sl(3): ad(diag(h1, h2, h3)) E_ij = (h_i - h_j) E_ij")
    print(f"   (checked with matrices for H = diag(3, 1, -4): "
          f"{ad_check((3, 1, -4))})")
    for i, j in sl3_roots():
        x, y = root_vector(i, j)
        angle = math.degrees(math.atan2(y, x)) % 360
        print(f"   e{i + 1} - e{j + 1}: angle {angle:6.1f} deg, length "
              f"{math.hypot(x, y):.4f}")
    simple = [root_vector(0, 1), root_vector(1, 2)]
    print(f"   simple roots e1 - e2, e2 - e3: Cartan matrix "
          f"{cartan_matrix(simple)}")
    print()
    print("Epistemic status: exact integer and rational computation for n <= 8")
    print("and for sl(3). It checks the classification for small n; the proof")
    print("that every irreducible representation is some V_n is in the lesson.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Explore

Explore: one-parameter subgroups of SL(2, ℝ)

A matrix $X \in \mathfrak{sl}(2, \R)$ generates the flow $v \mapsto e^{tX}v$ on the plane, whose trajectories are the orbits of the one-parameter subgroup. Theorem 6 sorts them by $\delta = -\det X$ . For $X = f - e$ ( $\delta < 0$ ) the flow is elliptic: closed orbits, a centre, and $e^{tX}$ is a rotation with $|\operatorname{tr}| \le 2$ . For $X = h$ ( $\delta > 0$ ) it is hyperbolic: a saddle, $\operatorname{tr} e^{tX} = 2\cosh t > 2$ . Change the equations to $x' = y$ , $y' = 0$ ( $X = e$ , $\delta = 0$ ) to see the parabolic shear flow. In the trace–determinant diagram, every trace-zero matrix sits on the vertical axis.

Elliptic: X = f − e

exp(tX) is rotation by t; orbits are circles.

Examples

x′ = −y, y′ = x

darker, longer arrows = faster forward in time backward in timeequilibrium (hollow = stable or centre)

Click the plane to start a trajectory, or type a start point below.

Start pointx₀y₀

Trajectories: 0. They are numerical approximations (fourth-order Runge–Kutta), not exact formulas.

Linear systemA = [0−110]

T = 0, D = 1, T² − 4D = −4; λ = 0 ± 1i

Equilibrium at (0, 0): centre: closed orbits around it

Trace T and determinant D: below the T-axis, saddles; above the dashed parabola D = T²/4, spirals; between them, nodes; on the upper D-axis, centres. Left of the D-axis is stable, right is unstable.

Hyperbolic: X = h

exp(tX) = diag(eᵗ, e⁻ᵗ); orbits are hyperbolas xy = const.

Examples

x′ = x, y′ = −y

darker, longer arrows = faster forward in time backward in timeequilibrium (hollow = stable or centre)

Click the plane to start a trajectory, or type a start point below.

Start pointx₀y₀

Trajectories: 0. They are numerical approximations (fourth-order Runge–Kutta), not exact formulas.

Linear systemA = [100−1]

T = 0, D = −1, T² − 4D = 4; λ = −1, 1

Equilibrium at (0, 0): saddle (unstable)

Trace T and determinant D: below the T-axis, saddles; above the dashed parabola D = T²/4, spirals; between them, nodes; on the upper D-axis, centres. Left of the D-axis is stable, right is unstable.

Non-commutativity in the group: compose a rotation and a shear in both orders.

AB ≠ BA in SL(2, ℝ)

Rotation by 90° and a shear: both have determinant 1, and their two composites differ.

A =

Set A to:

B =

Set B to:

First A, then B: the matrix BA

BA =

1−110

First B, then A: the matrix AB

AB =

0−111

image of the grid
image of the unit square
image of the flag
before the transformation
after the first step

AB ≠ BA: the order matters.

BA means “apply A first, then B”: products of transformations are read from right to left.

det(AB) = det(BA) = det A · det B = 1 · 1 = 1 The area scale factor is the same in either order.

Exercises

1. Lie groups and Lie algebras

Warm-upHuman

What is the dimension of $SU(3)$ as a real Lie group?

2. Lie groups and Lie algebras

Warm-upHuman

Which of these matrices belong to the Lie algebra $\mathfrak{su}(2)$ ? (Choose all that apply.)

Choose all that apply

\begin{pmatrix} i & 0 \\ 0 & -i \end{pmatrix}

\begin{pmatrix} 0 & 1 \\ -1 & 0 \end{pmatrix}

\begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}

\begin{pmatrix} i & 0 \\ 0 & i \end{pmatrix}

3. Lie groups and Lie algebras

CoreHuman

Which element of $SL(2, \R)$ is not of the form $e^X$ with $X \in \mathfrak{sl}(2, \R)$ ?

Choose one

\begin{pmatrix} -2 & 0 \\ 0 & -1/2 \end{pmatrix}

-I

\begin{pmatrix} 2 & 0 \\ 0 & 1/2 \end{pmatrix}

\begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}

4. Lie groups and Lie algebras

CoreHuman

$SU(2)$ and $SO(3)$ have isomorphic Lie algebras. Which property distinguishes the two groups?

Choose one

SU(2)

is simply connected, while

\pi_1(SO(3)) \cong \Z/2

Their dimensionsCompactnessConnectedness

5. Lie groups and Lie algebras

CoreHuman

In the classification of irreducible $\mathfrak{sl}(2, \C)$ -representations, why must the string $v, fv, f^2v, \dots$ eventually reach $0$ ?

Choose one

Its non-zero members are

h

-eigenvectors with distinct eigenvalues

\mu, \mu - 2, \mu - 4, \dots

, hence linearly independent, and

V

is finite-dimensionalBecause

f

is nilpotent as a matrix in

\mathfrak{sl}(2)

Because

\mu

is a natural numberBecause

V

is irreducible

6. Lie groups and Lie algebras

CoreHuman

In the representation $V_2 \otimes V_2$ of $\mathfrak{sl}(2, \C)$ , what is the dimension of the eigenspace of $h$ for the eigenvalue (weight) $0$ ?

7. Lie groups and Lie algebras

CoreHuman

Decompose $V_3 \otimes V_1$ into irreducible representations $V_n$ . List the values of $n$ that occur, separated by commas.

8. Lie groups and Lie algebras

StretchFormal

For real $n \times n$ matrices, with exp the matrix exponential, which of these Lean statements is false in general (so it could not be proved)?

Choose one

∀ X Y, exp (X + Y) = exp X * exp Y∀ X (s t : ℝ), exp ((s + t) • X) = exp (s • X) * exp (t • X)∀ A, Aᵀ = -A → (exp A)ᵀ * exp A = 1∀ X, exp (-X) * exp X = 1

9. Lie groups and Lie algebras

StretchComputational

Write exp_sl2(a, b, c) returning the matrix exponential of $X = \begin{pmatrix} a & b \\ c & -a \end{pmatrix}$ as a nested list, using $X^2 = \delta I$ with $\delta = a^2 + bc$ : $e^X = C(\delta) I + S(\delta) X$ , where $C = \cosh\sqrt\delta$ , $S = \sinh\sqrt\delta/\sqrt\delta$ if $\delta > 0$ ; $C = \cos\sqrt{-\delta}$ , $S = \sin\sqrt{-\delta}/\sqrt{-\delta}$ if $\delta < 0$ ; and $C = S = 1$ if $\delta = 0$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"The exponential map is always surjective." It is onto for compact connected groups and for $GL(n, \C)$ , but not in general. In $SL(2, \R)$ every exponential has trace $\ge -2$ , so $\operatorname{diag}(-2, -\tfrac12)$ is not an exponential (Theorem 6), even though $SL(2, \R)$ is connected. What is true is that the image of $\exp$ generates any connected Lie group (Theorem 3).

Misconception

"A Lie algebra determines its Lie group." It determines the simply connected group $\tilde G$ and, through it, the group up to a discrete central quotient. $SU(2)$ and $SO(3)$ have isomorphic Lie algebras but different centres ( $\{\pm I\}$ versus trivial) and different fundamental groups ( $0$ versus $\Z/2$ ). Likewise $\R$ and $S^1$ share the Lie algebra $\R$ .

Misconception

" $e^{X+Y} = e^Xe^Y$ ." Only when $X$ and $Y$ commute. In general $\log(e^Xe^Y) = X + Y + \tfrac12[X, Y] + \tfrac1{12}\big([X, [X, Y]] + [Y, [Y, X]]\big) + \cdots$ (the Baker–Campbell–Hausdorff formula), whose correction terms are all brackets — one more sign that the bracket carries the group's multiplication.

Misconception

"Every Lie subgroup is closed." The image of the line of irrational slope in the torus $T^2$ is a one-dimensional Lie subgroup whose closure is the whole torus. The Lie correspondence matches subalgebras with immersed connected subgroups; closed subgroups are automatically embedded (Cartan's theorem), but not every Lie subgroup is closed.

Misconception

"Representations of a Lie algebra are the same as representations of the group." They are for simply connected groups. For $SO(3)$ , only the $V_n$ with $n$ even integrate; the spin- $\frac12$ representation $V_1$ of $\mathfrak{so}(3) \otimes \C$ is a representation of $SU(2)$ but only a "projective representation" of $SO(3)$ .

ViewpointsH

Many ways of seeing

Geometry— Homogeneous spaces and Klein's programme

Klein's Erlangen programme (1872) defines a geometry by its group of symmetries, and Lie groups make this precise: a homogeneous space $G/H$ (with $H$ closed) is a manifold on which $G$ acts transitively, and the geometry is the study of $G$ -invariants. The sphere is $SO(n+1)/SO(n)$ , hyperbolic space is $SO^+(n, 1)/SO(n)$ , and the hyperbolic plane is $SL(2, \R)/SO(2)$ — the upper half-plane, on which $SL(2, \R)$ acts by Möbius transformations $z \mapsto (az + b)/(cz + d)$ , isometries of the metric $(dx^2 + dy^2)/y^2$ . The elliptic, parabolic and hyperbolic one-parameter subgroups of the visualization are rotations about a point, horocyclic translations and translations along a geodesic. Cartan's symmetric spaces are the homogeneous spaces whose geodesic symmetries are isometries; he classified them using Lie theory.

Topology— The topology of groups

A Lie group is a very special manifold. Its fundamental group is abelian; its tangent bundle is trivial (left translation of a basis of $\mathfrak g$ ), so by Poincaré–Hopf its Euler characteristic, if it is compact, is $0$ — hence $S^2$ is not a Lie group, while $S^1$ and $S^3 = SU(2)$ are (they are the only spheres of positive dimension that are). Hopf (1941) showed that the real cohomology of a compact connected Lie group is an exterior algebra on generators of odd degree: for $SU(2) = S^3$ one generator in degree $3$ , for $SU(n)$ generators in degrees $3, 5, \dots, 2n - 1$ . Every connected Lie group deformation retracts onto a maximal compact subgroup ( $SL(2, \R)$ onto $SO(2)$ , so $\pi_1(SL(2, \R)) = \Z$ ), and Bott periodicity computes the homotopy groups of $U(n)$ and $O(n)$ in a stable range. See algebraic topology.

Algebra— Structure theory of Lie algebras

The algebraist studies $\mathfrak g$ on its own. Engel's and Lie's theorems describe nilpotent and solvable Lie algebras (strictly upper triangular and upper triangular matrices); the Levi decomposition writes every finite-dimensional real Lie algebra as a solvable ideal plus a semisimple subalgebra. Cartan's criterion characterises semisimplicity by the non-degeneracy of the Killing form $B(X, Y) = \operatorname{tr}(\operatorname{ad}X\operatorname{ad}Y)$ , and semisimple complex Lie algebras are classified by root systems and Dynkin diagrams. Mathlib formalises much of this: Engel's theorem, the Killing form, Cartan subalgebras and root pairings. Representation theory continues through the universal enveloping algebra, Verma modules and the Weyl character formula.

Analysis— Harmonic analysis on groups

Haar measure makes analysis on groups possible. For $G = U(1)$ , the Peter–Weyl theorem is the completeness of Fourier series $\sum c_ne^{in\theta}$ ; for compact $G$ , $L^2(G)$ decomposes as $\bigoplus_\pi \pi \otimes \pi^*$ over the irreducible representations. For non-compact groups the story becomes the subject of Harish-Chandra's work: the Plancherel formula for $SL(2, \R)$ involves both a discrete series and a continuous series of infinite-dimensional unitary representations. The Laplacian of a Riemannian symmetric space is built from the Casimir operator, so its spectral theory is representation theory. See harmonic analysis.

Physics— Spin, angular momentum and gauge symmetry

In quantum mechanics a symmetry group acts by unitary operators on a Hilbert space of states, so states come in representations. The components of angular momentum satisfy $[J_x, J_y] = i\hbar J_z$ — up to a factor $i\hbar$ , the relations of $\mathfrak{so}(3)$ — and the raising and lowering operators $J_\pm = J_x \pm iJ_y$ play the roles of $e$ and $f$ . Theorem 9 is the quantisation of angular momentum: a spin- $j$ particle has $2j + 1$ states, with $j \in \frac12\Z_{\ge 0}$ . Gell-Mann and Ne'eman's "eightfold way" (1961) arranged hadrons in representations of $SU(3)$ , the octet being the adjoint representation, whose weight diagram is the hexagon of roots above plus two weights at the centre. The Standard Model is a gauge theory with group $U(1) \times SU(2) \times SU(3)$ . These are physical models whose success is empirical; the mathematics of their representations is exact. See gauge theory.

Number theory— Arithmetic groups and the Langlands dual

Number theory meets Lie groups through arithmetic subgroups such as $SL(2, \Z) \subset SL(2, \R)$ . Modular forms are functions on $SL(2, \Z)\backslash SL(2, \R)$ with prescribed behaviour, and the Laplacian on $SL(2, \Z)\backslash\mathbb H$ has a continuous spectrum, described by Eisenstein series whose constant terms involve the Riemann zeta function, and a discrete spectrum (Maass forms) related to the lengths of closed geodesics by the Selberg trace formula. In the Langlands programme, each reductive group $G$ has a dual group $G^\vee$ whose root system exchanges roots and coroots — so $SO(2n+1)$ (type $B_n$ ) is dual to $Sp(2n, \C)$ (type $C_n$ ), $GL(n)$ is its own dual and $SL(n)$ is dual to $PGL(n)$ — and automorphic representations of $G$ are conjecturally parametrised by representations of the Galois group into $G^\vee$ . See the Langlands programme.

History & global context

History and global context

Lie's continuous groups. Sophus Lie, in Christiania (Oslo) and later Leipzig, developed "continuous transformation groups" from the 1870s to solve differential equations by symmetry, working closely with Felix Klein, whose Erlangen programme (1872) put groups at the centre of geometry. Lie and Friedrich Engel's Theorie der Transformationsgruppen (1888–93) set out the infinitesimal theory.
Classification. Wilhelm Killing classified the complex simple Lie algebras (1888–90), discovering the exceptional algebras, with some gaps; Élie Cartan's thesis (1894) completed and corrected the classification, and he later classified the real forms (1914) and the symmetric spaces (1926). Eugene Dynkin's diagrams (1946–47) gave the classification its modern combinatorial form.
Representations and compact groups. Hermann Weyl's papers of 1925–26 created the representation theory of compact Lie groups, with the character formula and the unitarian trick; the Peter–Weyl theorem followed in 1927. Alfréd Haar constructed invariant measures in 1933, and John von Neumann proved their uniqueness. Claude Chevalley's Theory of Lie Groups (1946) gave the global, manifold-theoretic foundations.
Hilbert's fifth problem and beyond. Andrew Gleason, Deane Montgomery and Leo Zippin (1952), with Hidehiko Yamabe's extension (1953), characterised Lie groups among topological groups. Harish-Chandra, working in the United States after training in India and Cambridge, developed the harmonic analysis of semisimple Lie groups from the 1950s to the 1970s. Robert Langlands's letter to André Weil (1967) began the programme that bears his name.

Continuous symmetry

Infinitesimal rotations and their commutators

Lie groups, Lie algebras and the exponential map

The classical groups and their Lie algebras

The Lie algebra and the exponential map

What the Lie algebra does not see

Compact groups, Haar measure and complete reducibility

The representations of sl(2, ℂ)

A first look at root systems: sl(3, ℂ)

Lie groups in Lean and Mathlib

Exponentials and representations, computed

Explore: one-parameter subgroups of SL(2, ℝ)

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading