## Formalized Name Highest Weight Classification for Compact Connected Lie Groups ## Formalized Statement Let $G$ be a compact connected Lie group with Lie algebra $\mathfrak g$, let $T\le G$ be a maximal torus with Lie algebra $\mathfrak t$, and let $X^*(T):=\operatorname{Hom}_{\mathrm{cts}}(T,S^1)$ be the character group of $T$. Let $\mathfrak g_{\mathbb C}:=\mathfrak g\otimes_{\mathbb R}\mathbb C$ and $\mathfrak t_{\mathbb C}:=\mathfrak t\otimes_{\mathbb R}\mathbb C$. Let $R\subset X^*(T)$ be the root system of $\mathfrak g_{\mathbb C}$ with respect to $\mathfrak t_{\mathbb C}$, choose a positive root system $R^+\subset R$, and for each $\alpha\in R$ let $\alpha^\vee$ denote the corresponding coroot. Define the dominant integral weights for $(G,T,R^+)$ by $X^*(T)^+:=\{\lambda\in X^*(T):\langle \lambda,\alpha^\vee\rangle\ge 0\text{ for every }\alpha\in R^+\}$. For an irreducible continuous finite-dimensional complex representation $\rho:G\to GL(V)$, let $\lambda_V\in X^*(T)$ denote the maximal $T$-weight of $V$ with respect to the partial order generated by $R^+$, equivalently the weight of any non-zero vector annihilated by all positive root spaces in the differentiated $\mathfrak g_{\mathbb C}$-module. If $\operatorname{Irr}(G)$ denotes the set of isomorphism classes of irreducible continuous finite-dimensional complex representations of $G$, then the assignment $[V]\mapsto \lambda_V$ defines a bijection from $\operatorname{Irr}(G)$ onto $X^*(T)^+$. ## Proof [proofplan] We decompose the restriction of an irreducible representation to the maximal torus and choose a maximal weight in the positive-root order. Root spaces raise weights, so positive root spaces annihilate the maximal weight space, and rank-one $\mathfrak{sl}_2$ theory proves dominance. Injectivity follows from highest-weight uniqueness for complex reductive Lie algebras, with the central character included because the weight is a character of the full maximal torus. Surjectivity is proved by constructing the irreducible highest-weight module for $\mathfrak g_{\mathbb C}$, integrating it to the simply connected Lie group with Lie algebra $\mathfrak g$, and using the fact that $\lambda$ is a genuine character of $T$ to show that the kernel of the universal covering acts as the identity. [/proofplan] [step:Decompose the representation into torus weight spaces] Let \begin{align*} \rho:G\to GL(V) \end{align*} be an irreducible continuous finite-dimensional complex representation. Since $G$ is compact, the unitarisation theorem for compact group representations gives a $G$-invariant Hermitian inner product on $V$. Restricting $\rho$ to the compact torus $T$, the weight decomposition theorem for compact tori gives a finite direct sum \begin{align*} V=\bigoplus_{\mu\in X^*(T)}V_\mu, \end{align*} where \begin{align*} V_\mu=\{v\in V:\rho(t)v=\mu(t)v\text{ for every }t\in T\}. \end{align*} Only finitely many $V_\mu$ are non-zero. Define \begin{align*} \operatorname{Wt}(V):=\{\mu\in X^*(T):V_\mu\ne 0\} \end{align*} to be the finite set of $T$-weights occurring in $V$. [/step] [step:Show that a maximal torus weight is killed by all positive root spaces] Define a partial order $\preceq$ on $X^*(T)$ by declaring that $\mu\preceq\nu$ if $\nu-\mu$ is a non-negative integral linear combination of elements of $R^+$. Since $\operatorname{Wt}(V)$ is finite, choose a maximal element $\lambda\in\operatorname{Wt}(V)$. Let \begin{align*} d\rho:\mathfrak g_{\mathbb C}\to\mathfrak{gl}(V) \end{align*} denote the complex-linear extension of the differentiated representation. If $X\in\mathfrak g_\alpha$, $v\in V_\mu$, and $H\in\mathfrak t_{\mathbb C}$, then the Lie algebra representation identity gives \begin{align*} d\rho(H)d\rho(X)v=d\rho(X)d\rho(H)v+d\rho([H,X])v. \end{align*} Because $v$ has weight $\mu$ and $X$ has root $\alpha$, this becomes \begin{align*} d\rho(H)d\rho(X)v=(\mu(H)+\alpha(H))d\rho(X)v. \end{align*} Thus \begin{align*} d\rho(X)V_\mu\subset V_{\mu+\alpha}. \end{align*} For $\alpha\in R^+$, the weight $\lambda+\alpha$ is strictly larger than $\lambda$ in the order $\preceq$, so maximality gives $V_{\lambda+\alpha}=0$. Hence \begin{align*} d\rho(\mathfrak g_\alpha)V_\lambda=0 \end{align*} for every $\alpha\in R^+$. [guided] Define the order $\preceq$ on $X^*(T)$ by declaring $\mu\preceq\nu$ exactly when $\nu-\mu$ is a sum of positive roots with coefficients in $\mathbb Z_{\ge 0}$. The weight set $\operatorname{Wt}(V)$ is finite by the torus weight decomposition, so it has a maximal element for this order. Choose one and call it $\lambda$. Now we verify that the root spaces move weights in the expected direction. Let $X\in\mathfrak g_\alpha$, let $v\in V_\mu$, and let $H\in\mathfrak t_{\mathbb C}$. Since $d\rho$ is a Lie algebra representation, \begin{align*} d\rho(H)d\rho(X)v=d\rho(X)d\rho(H)v+d\rho([H,X])v. \end{align*} The condition $v\in V_\mu$ means that the differentiated torus action satisfies $d\rho(H)v=\mu(H)v$. The condition $X\in\mathfrak g_\alpha$ means $[H,X]=\alpha(H)X$. Substituting these two identities gives \begin{align*} d\rho(H)d\rho(X)v=(\mu(H)+\alpha(H))d\rho(X)v. \end{align*} Therefore $d\rho(X)v$ is either zero or a vector of weight $\mu+\alpha$, which is exactly the inclusion \begin{align*} d\rho(X)V_\mu\subset V_{\mu+\alpha}. \end{align*} Apply this with $\mu=\lambda$ and $\alpha\in R^+$. Since $\lambda+\alpha$ is larger than $\lambda$ in the positive-root order, maximality of $\lambda$ forces $V_{\lambda+\alpha}=0$. Thus every positive root vector annihilates $V_\lambda$: \begin{align*} d\rho(\mathfrak g_\alpha)V_\lambda=0. \end{align*} So every non-zero vector in $V_\lambda$ is a highest weight vector. [/guided] [/step] [step:Use rank-one subalgebras to prove dominance of the highest weight] Let $\alpha\in R^+$. Choose elements $E_\alpha\in\mathfrak g_\alpha$, $F_\alpha\in\mathfrak g_{-\alpha}$, and $H_\alpha\in\mathfrak t_{\mathbb C}$ that form an $\mathfrak{sl}_2(\mathbb C)$-triple, with $H_\alpha$ corresponding to the coroot $\alpha^\vee$. Restricting $d\rho$ to the span of $E_\alpha,F_\alpha,H_\alpha$ gives a finite-dimensional $\mathfrak{sl}_2(\mathbb C)$-module. Choose $0\ne v\in V_\lambda$. The previous step gives $d\rho(E_\alpha)v=0$, and $v$ is an eigenvector for $d\rho(H_\alpha)$ with eigenvalue \begin{align*} \lambda(H_\alpha)=\langle\lambda,\alpha^\vee\rangle. \end{align*} The finite-dimensional representation theory of $\mathfrak{sl}_2(\mathbb C)$ says that the highest eigenvalue of such a vector is a non-negative integer. Therefore \begin{align*} \langle\lambda,\alpha^\vee\rangle\in\mathbb Z_{\ge 0}. \end{align*} Since this holds for every $\alpha\in R^+$, we have $\lambda\in X^*(T)^+$. [/step] [step:Prove that the highest weight determines the irreducible representation] Let \begin{align*} \rho_i:G\to GL(V_i) \end{align*} for $i\in\{1,2\}$ be irreducible continuous finite-dimensional complex representations with the same highest weight $\lambda\in X^*(T)^+$. Since $G$ is compact, the Lie algebra $\mathfrak g$ is compact real reductive, so $\mathfrak g_{\mathbb C}$ is a complex reductive Lie algebra. The chosen positive roots define a Borel subalgebra \begin{align*} \mathfrak b:=\mathfrak t_{\mathbb C}\oplus\bigoplus_{\alpha\in R^+}\mathfrak g_\alpha. \end{align*} The highest-weight uniqueness theorem for finite-dimensional modules over a complex reductive Lie algebra applies because $V_1$ and $V_2$ are irreducible finite-dimensional $\mathfrak g_{\mathbb C}$-modules, $\mathfrak g_{\mathbb C}$ is reductive, and the highest weight is specified as a functional on the full Cartan subalgebra $\mathfrak t_{\mathbb C}$. This last point includes the central character: on the centre of $\mathfrak g_{\mathbb C}$, root spaces do not contribute, and the action is determined by the same differential of the character $\lambda:T\to S^1$. Hence there exists a complex-linear isomorphism \begin{align*} A:V_1\to V_2 \end{align*} such that \begin{align*} A d\rho_1(X)=d\rho_2(X)A \end{align*} for every $X\in\mathfrak g_{\mathbb C}$. Define \begin{align*} H:=\{g\in G:A\rho_1(g)=\rho_2(g)A\}. \end{align*} Then $H$ is a closed subgroup of $G$. Its Lie algebra contains $\mathfrak g$ because $A$ intertwines the differentiated representations. Since $G$ is connected, the only closed subgroup with Lie algebra containing $\mathfrak g$ is $G$ itself. Therefore $A$ is a $G$-module isomorphism, and the highest-weight map is injective. [/step] [step:Construct the irreducible representation with a prescribed dominant weight] Let $\lambda\in X^*(T)^+$. Since $G$ is compact, $\mathfrak g_{\mathbb C}$ is a complex reductive Lie algebra. The finite-dimensional highest-weight existence theorem for complex reductive Lie algebras applies to $\mathfrak g_{\mathbb C}$ with Cartan subalgebra $\mathfrak t_{\mathbb C}$ and positive roots $R^+$: the hypotheses are that $\mathfrak g_{\mathbb C}$ is reductive and that the proposed highest weight is integral and dominant on each root $\mathfrak{sl}_2$-subalgebra. Dominance is part of $\lambda\in X^*(T)^+$, and integrality follows because $\lambda$ is a character of the torus $T$. Thus there is an irreducible finite-dimensional $\mathfrak g_{\mathbb C}$-module $V(\lambda)$ with highest weight $\lambda$. Let \begin{align*} \pi:\widehat G\to G \end{align*} be the universal covering homomorphism of the connected Lie group $G$, and let $K:=\ker\pi$. Let $\widehat T_0$ denote the connected Lie subgroup of $\widehat G$ with Lie algebra $\mathfrak t$. The standard integration theorem for finite-dimensional Lie algebra representations of simply connected Lie groups applies because $\widehat G$ is connected and simply connected with Lie algebra $\mathfrak g$; hence the underlying real Lie algebra representation of $V(\lambda)$ integrates uniquely to a continuous representation \begin{align*} \widehat\rho_\lambda:\widehat G\to GL(V(\lambda)). \end{align*} The subgroup $K$ is discrete and central in $\widehat G$, and $K\cap\widehat T_0$ is the kernel of the covering map $\widehat T_0\to T$. We show that $K$ acts as the identity. Since every element of $K$ is central and every element of a compact connected Lie group is conjugate into a maximal torus after applying $\pi$, the centrality of $K$ allows the descent test to be checked on $K\cap\widehat T_0$. The highest $\widehat T_0$-weight of $V(\lambda)$ is the pullback of $\lambda$ along $\widehat T_0\to T$, so it is trivial on $K\cap\widehat T_0$. Every other weight of $V(\lambda)$ has the form \begin{align*} \lambda-\sum_{\alpha\in R^+}n_\alpha\alpha \end{align*} with $n_\alpha\in\mathbb Z_{\ge 0}$ and only finitely many non-zero $n_\alpha$. Each root $\alpha$ is trivial on $K\cap\widehat T_0$, because roots are the non-trivial characters by which the torus acts on the adjoint root spaces, while elements of $K$ act trivially under the adjoint action. Hence every weight of $V(\lambda)$ is trivial on $K\cap\widehat T_0$, and therefore $K$ acts as the identity on every weight space. The descent criterion for covering groups now applies: a representation of $\widehat G$ factors through $G=\widehat G/K$ exactly when $K$ acts as the identity. Therefore there is a unique continuous representation \begin{align*} \rho_\lambda:G\to GL(V(\lambda)) \end{align*} such that $\widehat\rho_\lambda=\rho_\lambda\circ\pi$. Its differentiated $\mathfrak g_{\mathbb C}$-module is $V(\lambda)$, which is irreducible. Since $G$ is connected, any non-zero $G$-stable subspace would be a non-zero $\mathfrak g_{\mathbb C}$-submodule, so $\rho_\lambda$ is irreducible. Its highest weight is $\lambda$ by construction. [guided] We begin with a dominant character $\lambda\in X^*(T)^+$. The phrase dominant character contains both pieces of information needed for construction. First, $\lambda$ is an actual continuous character $T\to S^1$, so its differential is integral on the torus lattice. Second, for every positive root $\alpha\in R^+$, the coroot pairing satisfies \begin{align*} \langle\lambda,\alpha^\vee\rangle\ge 0. \end{align*} Together these say exactly that the restriction of $\lambda$ to each root $\mathfrak{sl}_2(\mathbb C)$ has a non-negative integral highest weight. Since $G$ is compact, its Lie algebra is compact real reductive, and therefore $\mathfrak g_{\mathbb C}$ is a complex reductive Lie algebra. We apply the standard highest-weight existence theorem for finite-dimensional modules over complex reductive Lie algebras to $\mathfrak g_{\mathbb C}$, the Cartan subalgebra $\mathfrak t_{\mathbb C}$, and the positive system $R^+$. The theorem requires a dominant integral weight on the full Cartan subalgebra. The root directions are handled by the inequalities defining $X^*(T)^+$, and the central directions are handled because $\lambda$ is a character of the full torus $T$, not merely a weight for the derived algebra. Hence the theorem produces an irreducible finite-dimensional $\mathfrak g_{\mathbb C}$-module $V(\lambda)$ with highest weight $\lambda$. Next we must prove that this Lie algebra module comes from the particular group $G$. Let \begin{align*} \pi:\widehat G\to G \end{align*} be the universal covering homomorphism, and define $K:=\ker\pi$. The group $\widehat G$ is connected and simply connected with Lie algebra $\mathfrak g$. The standard integration theorem for finite-dimensional Lie algebra representations of simply connected Lie groups says that every finite-dimensional representation of $\mathfrak g$ integrates uniquely to a representation of $\widehat G$. Applying this theorem to the underlying real representation of $V(\lambda)$ gives \begin{align*} \widehat\rho_\lambda:\widehat G\to GL(V(\lambda)). \end{align*} The remaining question is descent through the covering map. A representation of $\widehat G$ descends to $G=\widehat G/K$ exactly when every element of $K$ acts as the identity. Let $\widehat T_0$ be the connected Lie subgroup of $\widehat G$ with Lie algebra $\mathfrak t$. The map $\widehat T_0\to T$ induced by $\pi$ is a covering of tori, and $K\cap\widehat T_0$ is its kernel. Since the highest weight of $V(\lambda)$ on $\widehat T_0$ is the pullback of the character $\lambda:T\to S^1$, that highest weight is trivial on $K\cap\widehat T_0$. Now examine all other weights. In a highest-weight module, every weight is obtained from the highest weight by subtracting a finite non-negative integral combination of positive roots, so each weight has the form \begin{align*} \lambda-\sum_{\alpha\in R^+}n_\alpha\alpha, \end{align*} where $n_\alpha\in\mathbb Z_{\ge 0}$ and all but finitely many $n_\alpha$ are zero. If $k\in K\cap\widehat T_0$, then $k$ is central in $\widehat G$, so its adjoint action on every root space is the identity. But the root $\alpha$ is precisely the character by which $\widehat T_0$ acts on the root space $\mathfrak g_\alpha$ under the adjoint representation. Therefore $\alpha(k)=1$ for every root $\alpha$ and every $k\in K\cap\widehat T_0$. The highest weight is trivial on $K\cap\widehat T_0$, and every root is trivial on $K\cap\widehat T_0$. Hence every weight of $V(\lambda)$ is trivial on $K\cap\widehat T_0$. Since $V(\lambda)$ decomposes into $\widehat T_0$-weight spaces, each element of $K\cap\widehat T_0$ acts as the identity on every weight space. Centrality then gives trivial action of the full kernel $K$ in the descent test. Thus $\widehat\rho_\lambda$ factors uniquely through $G$, giving a representation \begin{align*} \rho_\lambda:G\to GL(V(\lambda)). \end{align*} Finally, if $W\subset V(\lambda)$ were a non-zero proper $G$-stable subspace, then differentiating the action would make $W$ a non-zero proper $\mathfrak g_{\mathbb C}$-submodule. This contradicts irreducibility of $V(\lambda)$. Therefore $\rho_\lambda$ is irreducible and has highest weight $\lambda$. [/guided] [/step] [step:Conclude that the highest-weight map is bijective] The first three steps show that every irreducible continuous finite-dimensional complex representation of $G$ has a highest weight in $X^*(T)^+$. The uniqueness step proves that two irreducible representations with the same highest weight are isomorphic. The construction step proves that every $\lambda\in X^*(T)^+$ occurs as the highest weight of an irreducible representation of $G$. Therefore the map \begin{align*} \operatorname{Irr}(G)\to X^*(T)^+ \end{align*} sending an irreducible representation to its highest weight is bijective. [/step]