## Formalized Name Highest Weight Classification Theorem 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,U(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}$, identifying each root character with its complex-linear differential on $\mathfrak t_{\mathbb C}$. Choose a positive root system $R^+\subset R$, and let $\Delta\subset R^+$ be the corresponding set of simple roots. For each $\alpha\in R$, let $\alpha^\vee$ denote its coroot. Define $\Lambda^+(G,T,R^+)$ to be the set of all $\lambda\in X^*(T)$ such that $\langle \lambda,\alpha^\vee\rangle\in\mathbb Z_{\ge 0}$ for every $\alpha\in\Delta$. For every continuous irreducible finite-dimensional complex representation $\rho:G\to GL(V)$, the restricted representation $\rho|_T$ has a finite $T$-weight set in $X^*(T)$, ordered by declaring $\mu\le \nu$ when $\nu-\mu$ is a finite $\mathbb Z_{\ge 0}$-linear combination of elements of $R^+$. With respect to this order, $\rho$ has a unique highest weight $\lambda_\rho\in\Lambda^+(G,T,R^+)$. The assignment $[(\rho,V)]\mapsto \lambda_\rho$ defines a bijection from the set of isomorphism classes of continuous irreducible finite-dimensional complex representations of $G$ onto $\Lambda^+(G,T,R^+)$. ## Proof [proofplan] We decompose a finite-dimensional representation into $T$-weight spaces and use the standard highest-weight theorem for irreducible modules over the complex reductive Lie algebra $\mathfrak g_{\mathbb C}$ to obtain the highest weight and prove injectivity. For surjectivity, we construct the irreducible $\mathfrak g_{\mathbb C}$-module with prescribed full highest weight, including the action of the complexified center. We then integrate this infinitesimal module to the simply connected universal cover of $G$ and use the fact that the chosen highest weight is an actual character of $T$ to prove that the covering kernel acts as the identity. This descends the representation to $G$ and completes the bijection. [/proofplan] [step:Define the highest weight map from torus weights] Let $(\rho,V)$ be a continuous irreducible finite-dimensional complex representation of $G$. By averaging a Hermitian inner product over the compact group $G$ using Haar probability measure, we may choose a Hermitian inner product $(\cdot,\cdot)_V$ on $V$ for which every operator $\rho(g):V\to V$ is unitary. Since $T$ is compact and abelian, the weight-space decomposition for compact tori gives a finite subset $\operatorname{Wt}(V)\subset X^*(T)$ and a direct sum decomposition \begin{align*} V=\bigoplus_{\nu\in \operatorname{Wt}(V)}V_\nu \end{align*} where \begin{align*} V_\nu:=\{v\in V:\rho(t)v=\nu(t)v\text{ for every }t\in T\}. \end{align*} The order in the theorem statement is a partial order on this finite set. The standard highest-weight theorem for irreducible finite-dimensional representations of compact connected Lie groups, in its infinitesimal form for the complex reductive Lie algebra $\mathfrak g_{\mathbb C}$, applies because $G$ is compact and connected, $T$ is a maximal torus, and $R^+$ is a positive system. It says that an irreducible finite-dimensional $G$-representation has a unique maximal $T$-weight, that this weight has multiplicity one, and that it is dominant with respect to $R^+$. Denote this unique maximal weight by $\lambda_\rho$. Dominance gives \begin{align*} \langle \lambda_\rho,\alpha^\vee\rangle\in\mathbb Z_{\ge 0} \end{align*} for every $\alpha\in\Delta$, so $\lambda_\rho\in\Lambda^+(G,T,R^+)$. Isomorphic representations have the same restricted $T$-weight spaces, so $[(\rho,V)]\mapsto\lambda_\rho$ is well-defined on isomorphism classes. [/step] [step:Prove injectivity by differentiating to irreducible highest-weight modules] Let $(\rho,V)$ and $(\sigma,W)$ be irreducible finite-dimensional complex representations of $G$ with common highest weight $\lambda\in\Lambda^+(G,T,R^+)$. Write $\mathfrak{gl}(V):=\operatorname{End}_{\mathbb C}(V)$ and $\mathfrak{gl}(W):=\operatorname{End}_{\mathbb C}(W)$ for the complex Lie algebras of linear endomorphisms. Define \begin{align*} d\rho_{\mathbb C}:\mathfrak g_{\mathbb C}\to\mathfrak{gl}(V) \end{align*} to be the complex-linear extension of the differential of $\rho$, and define \begin{align*} d\sigma_{\mathbb C}:\mathfrak g_{\mathbb C}\to\mathfrak{gl}(W) \end{align*} analogously. We first check irreducibility after differentiation. If $V_0\subset V$ is a non-zero $\mathfrak g_{\mathbb C}$-invariant complex subspace, then it is invariant under $d\rho(X)$ for every $X\in\mathfrak g$. Hence it is invariant under $\rho(\exp_G X)$ for every $X\in\mathfrak g$, because the exponential series for $\rho(\exp_G X)$ is the exponential of $d\rho(X)$. The subgroup generated by $\exp_G(\mathfrak g)$ is all of $G$ since $G$ is connected. Thus $V_0$ is $G$-invariant, and irreducibility of $(\rho,V)$ gives $V_0=V$. Therefore $V$ is irreducible as a $\mathfrak g_{\mathbb C}$-module. The same argument shows that $W$ is irreducible as a $\mathfrak g_{\mathbb C}$-module. For a character $\chi\in X^*(T)$, let \begin{align*} d\chi_e:\mathfrak t\to i\mathbb R \end{align*} denote its real differential at the identity element $e\in T$, and let \begin{align*} d\chi_{e,\mathbb C}:\mathfrak t_{\mathbb C}\to\mathbb C \end{align*} denote the complex-linear extension of $d\chi_e$. The $T$-weights of $V$ and $W$ differentiate to the $\mathfrak t_{\mathbb C}$-weights of the modules $V$ and $W$, and the highest weight in both cases is $d\lambda_{e,\mathbb C}$. The finite-dimensional highest-weight classification theorem for complex reductive Lie algebras states the following form needed here: if $\mathfrak a$ is a complex reductive Lie algebra, $\mathfrak h\subset\mathfrak a$ is a Cartan subalgebra, a positive root system is fixed, and the action of $Z(\mathfrak a)$ is prescribed by the restriction of a highest weight to $Z(\mathfrak a)$, then there is at most one irreducible finite-dimensional $\mathfrak a$-module with that highest weight. Its hypotheses hold for $\mathfrak a=\mathfrak g_{\mathbb C}$ and $\mathfrak h=\mathfrak t_{\mathbb C}$ because the complexification of the Lie algebra of a compact connected Lie group is reductive, $\mathfrak t_{\mathbb C}$ is a Cartan subalgebra, and $R^+$ supplies the positive roots. Therefore there exists a complex-linear isomorphism \begin{align*} A:V\to W \end{align*} such that \begin{align*} A d\rho_{\mathbb C}(Y)=d\sigma_{\mathbb C}(Y)A \end{align*} for every $Y\in\mathfrak g_{\mathbb C}$. Define \begin{align*} \rho_A:G\to GL(W) \end{align*} by \begin{align*} \rho_A(g)=A\rho(g)A^{-1}. \end{align*} Then $d(\rho_A)_e=d\sigma_e$. The standard uniqueness theorem for Lie group homomorphisms says that two homomorphisms from a connected Lie group to a Lie group with the same differential at the identity are equal. Applying this to $\rho_A$ and $\sigma$ gives $\rho_A(g)=\sigma(g)$ for every $g\in G$. Hence $A\rho(g)=\sigma(g)A$ for every $g\in G$, so $(\rho,V)\cong(\sigma,W)$. [guided] We must prove that equality of highest weights determines the original group representation, not only a list of torus eigenvalues. Let $(\rho,V)$ and $(\sigma,W)$ be irreducible finite-dimensional complex representations of $G$ with common highest weight $\lambda$. Define \begin{align*} d\rho_{\mathbb C}:\mathfrak g_{\mathbb C}\to\mathfrak{gl}(V) \end{align*} to be the complex-linear extension of the differential of $\rho$, and define \begin{align*} d\sigma_{\mathbb C}:\mathfrak g_{\mathbb C}\to\mathfrak{gl}(W) \end{align*} in the same way. Before applying highest-weight theory for Lie algebras, we must verify that these differentiated modules are irreducible. Suppose $V_0\subset V$ is a non-zero complex subspace invariant under $d\rho_{\mathbb C}(\mathfrak g_{\mathbb C})$. Then $V_0$ is invariant under $d\rho(X)$ for every $X\in\mathfrak g$. Since the representation of the one-parameter subgroup $s\mapsto\rho(\exp_G(sX))$ is obtained by exponentiating $s d\rho(X)$, the subspace $V_0$ is invariant under $\rho(\exp_G X)$ for every $X\in\mathfrak g$. The connected Lie group $G$ is generated by its one-parameter subgroups, so $V_0$ is invariant under all of $G$. Because $(\rho,V)$ is irreducible as a $G$-representation, this forces $V_0=V$. Thus $V$ is irreducible as a $\mathfrak g_{\mathbb C}$-module. The same argument proves that $W$ is irreducible as a $\mathfrak g_{\mathbb C}$-module. For each character $\chi\in X^*(T)$, define \begin{align*} d\chi_e:\mathfrak t\to i\mathbb R \end{align*} to be the real differential of $\chi:T\to U(1)$ at $e\in T$, and define \begin{align*} d\chi_{e,\mathbb C}:\mathfrak t_{\mathbb C}\to\mathbb C \end{align*} to be its complex-linear extension. The $T$-weight condition $\rho(t)v=\chi(t)v$ differentiates to the $\mathfrak t_{\mathbb C}$-weight condition $d\rho_{\mathbb C}(H)v=d\chi_{e,\mathbb C}(H)v$ for $H\in\mathfrak t_{\mathbb C}$. Therefore the common group highest weight $\lambda$ becomes the common infinitesimal highest weight $d\lambda_{e,\mathbb C}$. Now apply the finite-dimensional highest-weight classification theorem for complex reductive Lie algebras in the following form: for a complex reductive Lie algebra $\mathfrak a$ with Cartan subalgebra $\mathfrak h$ and chosen positive roots, an irreducible finite-dimensional highest-weight module is uniquely determined by its highest weight, including the induced scalar action of the center $Z(\mathfrak a)$. The hypotheses are satisfied with $\mathfrak a=\mathfrak g_{\mathbb C}$ and $\mathfrak h=\mathfrak t_{\mathbb C}$ because compactness of $G$ implies reductivity of $\mathfrak g_{\mathbb C}$, and a maximal torus complexifies to a Cartan subalgebra. Thus there is a complex-linear isomorphism \begin{align*} A:V\to W \end{align*} intertwining the differentiated actions: \begin{align*} A d\rho_{\mathbb C}(Y)=d\sigma_{\mathbb C}(Y)A \end{align*} for every $Y\in\mathfrak g_{\mathbb C}$. It remains to pass from infinitesimal equivalence to group equivalence. Define \begin{align*} \rho_A:G\to GL(W) \end{align*} by \begin{align*} \rho_A(g)=A\rho(g)A^{-1}. \end{align*} The intertwining identity for $Y\in\mathfrak g\subset\mathfrak g_{\mathbb C}$ says exactly that $d(\rho_A)_e=d\sigma_e$. We now use the uniqueness theorem for Lie group homomorphisms from a connected domain: if two Lie group homomorphisms out of a connected Lie group have the same differential at the identity, then they agree everywhere. Since $G$ is connected, $\rho_A(g)=\sigma(g)$ for all $g\in G$. Equivalently, $A\rho(g)=\sigma(g)A$ for all $g\in G$. Therefore $A$ is an isomorphism of $G$-representations. [/guided] [/step] [step:Construct an irreducible infinitesimal module with prescribed full dominant weight] Let $\lambda\in\Lambda^+(G,T,R^+)$. Define \begin{align*} \eta:=d\lambda_{e,\mathbb C}:\mathfrak t_{\mathbb C}\to\mathbb C \end{align*} to be the complex-linear differential of the character $\lambda:T\to U(1)$ at the identity. Let \begin{align*} \mathfrak z_{\mathbb C}:=Z(\mathfrak g_{\mathbb C}) \end{align*} and \begin{align*} \mathfrak s_{\mathbb C}:=[\mathfrak g_{\mathbb C},\mathfrak g_{\mathbb C}]. \end{align*} The standard structure theorem for compact Lie algebras says that $\mathfrak g_{\mathbb C}$ is reductive and decomposes as \begin{align*} \mathfrak g_{\mathbb C}=\mathfrak z_{\mathbb C}\oplus\mathfrak s_{\mathbb C} \end{align*} where $\mathfrak s_{\mathbb C}$ is semisimple. Since every element of $\mathfrak z_{\mathbb C}$ commutes with $\mathfrak t_{\mathbb C}$ and $\mathfrak t_{\mathbb C}$ is a Cartan subalgebra of $\mathfrak g_{\mathbb C}$, we have $\mathfrak z_{\mathbb C}\subseteq\mathfrak t_{\mathbb C}$. Set \begin{align*} \mathfrak h_{\mathbb C}:=\mathfrak t_{\mathbb C}\cap\mathfrak s_{\mathbb C}. \end{align*} Then \begin{align*} \mathfrak t_{\mathbb C}=\mathfrak z_{\mathbb C}\oplus\mathfrak h_{\mathbb C}. \end{align*} The positive system $R^+$ is the root system of the semisimple algebra $\mathfrak s_{\mathbb C}$ with respect to $\mathfrak h_{\mathbb C}$. The restriction $\eta|_{\mathfrak h_{\mathbb C}}$ is dominant integral because $\langle\lambda,\alpha^\vee\rangle\in\mathbb Z_{\ge 0}$ for every simple root $\alpha\in\Delta$. By the finite-dimensional highest-weight existence theorem for complex semisimple Lie algebras, there exists an irreducible finite-dimensional $\mathfrak s_{\mathbb C}$-module $V_\lambda$ whose highest weight is $\eta|_{\mathfrak h_{\mathbb C}}$. Define an action of $\mathfrak g_{\mathbb C}=\mathfrak z_{\mathbb C}\oplus\mathfrak s_{\mathbb C}$ on $V_\lambda$ as follows: $S\in\mathfrak s_{\mathbb C}$ acts by the semisimple module action, and $Z\in\mathfrak z_{\mathbb C}$ acts by the scalar $\eta(Z)$. This is a Lie algebra representation because $\mathfrak z_{\mathbb C}$ is central and acts by scalars. Any non-zero subspace stable under $\mathfrak g_{\mathbb C}$ is stable under $\mathfrak s_{\mathbb C}$, so irreducibility as an $\mathfrak s_{\mathbb C}$-module implies irreducibility as a $\mathfrak g_{\mathbb C}$-module. If $v_\lambda\in V_\lambda$ is a non-zero highest-weight vector for the $\mathfrak s_{\mathbb C}$-action, then every $H\in\mathfrak t_{\mathbb C}$ has a unique decomposition $H=Z+H_s$ with $Z\in\mathfrak z_{\mathbb C}$ and $H_s\in\mathfrak h_{\mathbb C}$. Hence \begin{align*} H v_\lambda=\eta(Z)v_\lambda+\eta(H_s)v_\lambda. \end{align*} Since $\eta$ is linear and $H=Z+H_s$, this becomes \begin{align*} H v_\lambda=\eta(H)v_\lambda. \end{align*} The positive-root spaces are contained in $\mathfrak s_{\mathbb C}$, so they kill $v_\lambda$. Thus the constructed irreducible $\mathfrak g_{\mathbb C}$-module has full highest weight $\eta=d\lambda_{e,\mathbb C}$. [/step] [step:Integrate the infinitesimal module and descend through the universal cover] Let \begin{align*} q:\widetilde G\to G \end{align*} be the universal covering homomorphism of the connected Lie group $G$, and let \begin{align*} K:=\ker q. \end{align*} The group $\widetilde G$ is connected and simply connected, and $K$ is a discrete central subgroup of $\widetilde G$. The standard Lie integration theorem says that every finite-dimensional complex representation of the complexified Lie algebra $\mathfrak g_{\mathbb C}$, viewed as a real representation of $\mathfrak g$, integrates uniquely to a representation of the simply connected Lie group with Lie algebra $\mathfrak g$. Applying this theorem to the module $V_\lambda$ constructed above gives a representation \begin{align*} \widetilde\rho_\lambda:\widetilde G\to GL(V_\lambda). \end{align*} Let $\widetilde T\le\widetilde G$ denote the connected Lie subgroup with Lie algebra $\mathfrak t$. The restriction \begin{align*} q_T:\widetilde T\to T \end{align*} of $q$ to $\widetilde T$ is a covering homomorphism. We use the standard lattice theorem for compact connected Lie groups: for a maximal torus $T\le G$, the inclusion $T\hookrightarrow G$ induces a surjection on fundamental groups. Equivalently, for the universal cover $q:\widetilde G\to G$, the covering kernel satisfies \begin{align*} K\subseteq\widetilde T. \end{align*} Thus \begin{align*} K=\ker q_T. \end{align*} It remains to show that every $k\in K$ acts as the identity on $V_\lambda$. The $\widetilde T$-weights of $V_\lambda$ are obtained from the highest weight by subtracting non-negative integer combinations of roots. Hence each such weight has the form \begin{align*} \mu=\lambda-\sum_{\alpha\in R^+}m_\alpha\alpha \end{align*} where each $m_\alpha\in\mathbb Z_{\ge 0}$. Here $\mu$, $\lambda$, and every root $\alpha$ are characters of $T$, and we regard them as characters of $\widetilde T$ by composition with $q_T$. If $k\in K=\ker q_T$, then $q_T(k)=e$, so \begin{align*} \mu(q_T(k))=1. \end{align*} Therefore every $\widetilde T$-weight character occurring in $V_\lambda$ is trivial on $K$. Since the $\widetilde T$-action is diagonal on the direct sum of weight spaces, $\widetilde\rho_\lambda(k)$ is the identity on every weight space, and hence on all of $V_\lambda$. Thus $K\subseteq\ker\widetilde\rho_\lambda$. Therefore $\widetilde\rho_\lambda$ factors uniquely through $q$, giving a representation \begin{align*} \rho_\lambda:G\to GL(V_\lambda) \end{align*} such that $\widetilde\rho_\lambda=\rho_\lambda\circ q$. [guided] The subtle point is descent. The universal cover of $G$ need not be compact: if $G=S^1$, then the universal cover is $\mathbb R$. So we do not use compactness of $\widetilde G$. Instead, we use only the covering structure and the integral lattice supplied by the character group of the maximal torus. Let \begin{align*} q:\widetilde G\to G \end{align*} be the universal covering homomorphism, and define \begin{align*} K:=\ker q. \end{align*} Because $q$ is a covering homomorphism of connected Lie groups, $K$ is discrete. It is also central: for fixed $k\in K$, the map $\widetilde G\to K$ given by $x\mapsto xkx^{-1}$ is continuous, its domain is connected, and its codomain is discrete; hence it is constant, and evaluating at the identity gives $xkx^{-1}=k$ for all $x\in\widetilde G$. The infinitesimal module $V_\lambda$ is finite-dimensional, so the standard Lie integration theorem applies: every finite-dimensional representation of the Lie algebra $\mathfrak g$ integrates uniquely to the simply connected Lie group with Lie algebra $\mathfrak g$. Since $\widetilde G$ is simply connected and has Lie algebra $\mathfrak g$, we obtain a representation \begin{align*} \widetilde\rho_\lambda:\widetilde G\to GL(V_\lambda). \end{align*} Let $\widetilde T\le\widetilde G$ be the connected Lie subgroup with Lie algebra $\mathfrak t$, and let \begin{align*} q_T:\widetilde T\to T \end{align*} be the restriction of $q$. Since $T$ is connected and its Lie algebra is $\mathfrak t$, the image $q_T(\widetilde T)$ is the connected subgroup of $T$ with Lie algebra $\mathfrak t$, hence is all of $T$. Thus $q_T$ is a covering homomorphism. We now use the standard lattice theorem for compact connected Lie groups: the inclusion of a maximal torus $T\hookrightarrow G$ induces a surjection on fundamental groups. In covering-language this says exactly that every deck transformation in $K=\ker q$ is represented by a loop lying in $T$, or equivalently \begin{align*} K\subseteq\widetilde T. \end{align*} Since $q_T$ is the restriction of $q$, this gives \begin{align*} K=\ker q_T. \end{align*} Now we check the action of this kernel on the weight spaces. The $\widetilde T$-weights in the integrated highest-weight module are obtained from the highest weight by subtracting roots. Thus each weight has the form \begin{align*} \mu=\lambda-\sum_{\alpha\in R^+}m_\alpha\alpha \end{align*} with $m_\alpha\in\mathbb Z_{\ge 0}$. The crucial point is that these are not merely infinitesimal weights: $\lambda$ is an actual character of $T$ by hypothesis, and each root $\alpha$ is also a character of $T$. Therefore $\mu$ is an actual character of $T$. Pulling back along $q_T$ makes it a character of $\widetilde T$. If $k\in K$, then $k\in\ker q_T$, so $q_T(k)=e$. Hence every pulled-back character evaluates to $1$ on $k$: \begin{align*} \mu(q_T(k))=\mu(e)=1. \end{align*} The representation of the abelian group $\widetilde T$ is diagonal on its weight-space decomposition, and all diagonal characters are trivial on $K$. Therefore $\widetilde\rho_\lambda(k)$ is the identity on each weight space and hence on $V_\lambda$. We have proved $K\subseteq\ker\widetilde\rho_\lambda$. This is exactly the condition for a representation of $\widetilde G$ to factor through the quotient $\widetilde G/K\cong G$. Therefore there is a unique representation \begin{align*} \rho_\lambda:G\to GL(V_\lambda) \end{align*} satisfying $\widetilde\rho_\lambda=\rho_\lambda\circ q$. [/guided] [/step] [step:Verify irreducibility and identify the highest weight] The descended representation $(\rho_\lambda,V_\lambda)$ is irreducible. Indeed, if $U\subset V_\lambda$ is a non-zero $G$-invariant complex subspace, then $U$ is invariant under the differentiated $\mathfrak g_{\mathbb C}$-action. Since $V_\lambda$ was constructed as an irreducible $\mathfrak g_{\mathbb C}$-module, this forces $U=V_\lambda$. The highest-weight line in $V_\lambda$ is acted on by $T$ through the character $\lambda$, because its infinitesimal weight is $d\lambda_{e,\mathbb C}$ and the descent construction identifies the integrated torus character with the original character $\lambda$. Every other weight has the form $\lambda-\sum_{\alpha\in R^+}m_\alpha\alpha$ with at least one positive coefficient $m_\alpha$, so it is strictly lower than $\lambda$ in the dominance order. Therefore the highest weight of $(\rho_\lambda,V_\lambda)$ is $\lambda$. We have constructed, for each $\lambda\in\Lambda^+(G,T,R^+)$, an irreducible finite-dimensional complex representation of $G$ with highest weight $\lambda$. This proves surjectivity of the highest-weight assignment. Injectivity was proved above, so the assignment \begin{align*} [(\rho,V)]\mapsto\lambda_\rho \end{align*} is a bijection from isomorphism classes of irreducible finite-dimensional complex representations of $G$ onto $\Lambda^+(G,T,R^+)$. [/step]