Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Differentiation and integration of highest weights

Statement

Assume the Axiom of Choice. Let G be a compact connected Lie group, T a maximal torus with a fixed positive system, and s=[g,g]. All representations below are finite-dimensional complex representations, continuous in the group case. Differentiating a compact-group highest weight gives the same highest weight for the complexified derived Lie algebra: if π is an irreducible finite-dimensional representation of G with highest weight λX(T), then the associated sC-module has highest weight the restriction of the differential of λ to the derived Cartan algebra. Conversely, in general a module for gC alone contains no action of the connected centre and therefore does not by itself determine a representation of G. After choosing a representation of Z(G)0 commuting with the integrated Gdersc-action, the resulting representation of Z(G)0×Gdersc descends to G exactly when the finite central covering kernel acts trivially, equivalently when its weights on the preimage of T descend to characters in X(T).

Facts & Assumptions

Given: AC, the data in the Statement, and a fixed positive system.

[A1]

The Axiom of Choice The Axiom of Choice covers the choice assumptions of the following interfaces, including countable choice.

[L1]

Irreducible finite-dimensional continuous complex representations of G have highest weights in the dominant part of X(T) (Highest weights for compact connected groups).

[L2]

A torus character differentiates to a complex-linear functional on its complexified Lie algebra, with formula χ(expX)=edχ(X), and is determined by its differential (Characters are the integral weights).

[L3]

A Lie-algebra homomorphism from the Lie algebra of a connected simply connected real Lie group to that of a real Lie group integrates uniquely to a smooth group homomorphism (Lie's second fundamental theorem).

[L4]

Continuous Lie-group homomorphisms are smooth, exponentials are natural, and the exponential map is a local diffeomorphism at zero (Continuous homomorphisms between Lie groups are smooth, Exponential map is natural for Lie-group homomorphisms, The exponential map is a local diffeomorphism at zero).

[L5]

Multiplication gives a finite central covering p:H=Z(G)0×SG, where S=Gdersc is compact and simply connected with Lie algebra s (Compact connected Lie groups are classified by root data).

[L6]

A finite-dimensional continuous complex representation of a compact Lie group admits an invariant positive-definite Hermitian inner product (Finite-dimensional compact-group representations are unitarizable).

[L7]

Closed subgroups of Lie groups are embedded Lie subgroups, and a maximal torus in a compact connected Lie group is its own centralizer (Cartan closed subgroup theorem, The compact Weyl group is finite).

Proof

technique · direct
1.1

By [L4], π is smooth and π(expX)=exp(dπ(X)). An exponential neighborhood generates a connected group: the generated subgroup is open and its other cosets are open, so it is also closed and must be the whole group. Therefore a complex subspace invariant under the differential is group invariant, since the matrix exponential preserves it; the converse follows by differentiating. A commuting endomorphism of a nonzero irreducible complex representation is scalar: choose an eigenvalue, whose nonzero eigenspace is invariant and hence is the entire space. In particular Z(G)0 acts by scalars. Differentiating the covering in [L5] gives g=Lie(Z(G)0)s, with the first summand central. A subspace invariant under sC is consequently invariant under all of dπ and under G. Thus restriction to sC is irreducible.

L4L5algebra
1.2

Let v be a highest vector of π, of character λ from [L1]. Differentiating π(t)v=λ(t)v for tT gives dπ(X)v=dλ(X)v for Xt, and complex-linear extension gives the same identity on tC. Positive root operators annihilate v: such an operator takes a T-weight vector of character λ to one of character λα, by conjugating the differentiated action with tT, and a nonzero such weight would lie strictly above the highest weight. The derived Cartan weight is therefore the restriction of this complex-linear dλ to (ts)C.

L1L2L4algebra
1.3

Conversely let M be a finite-dimensional complex sC-module. Restrict its action to the real algebra s and apply [L3] with source S and target GLC(M) regarded as a real Lie group. This integrates the action uniquely to ρ:SGLC(M). Choose a continuous representation ζ:Z(G)0GLC(M) commuting with ρ. Then R(z,s)=ζ(z)ρ(s) is a representation of H. The derived-algebra data contain no prescribed action of the central factor; when that factor is trivial there is of course no extra choice. For M=0 every action and the resulting descent are the unique zero-dimensional ones.

L3L5givenalgebra
1.4

Write K=kerp. To justify the torus language, let U be the identity component of the closed Lie subgroup p1(T). The covering charts imply p(U) contains an identity neighborhood of T, hence equals connected T. For u,vU, their commutator lies in finite K; continuity on connected U×U makes it identity. Thus U is a compact connected abelian subgroup, hence a torus. It is maximal: a torus containing it maps to a torus containing T, so maps into T and lies in U. By [L7] central K lies in CH(U)=U. Since p(U)=T, every element of p1(T) differs from an element of U by one in K. Consequently p1(T)=U is a torus and U/K=T.

L5L7L4algebra
2.1

By [L6] the restriction RU is unitary. A finite-dimensional commuting family of unitary operators has a common orthonormal eigenbasis: if some operator is not scalar, its mutually orthogonal eigenspaces are preserved by every other operator, and induction on dimension diagonalizes the restrictions; if all are scalar any orthonormal basis suffices. The resulting diagonal entries are continuous characters χX(U). Since KU, it acts trivially on M exactly when every occurring character is trivial on K. Such a character factors uniquely through U/K=T, and the factor is continuous because the compact-to-Hausdorff surjection UT is a quotient map. Thus this is precisely the condition that all weights lie in pX(T). Conversely a pulled-back character is trivial on K. For the zero module the character family is empty and both conditions hold.

L2L6step 1.3step 1.4algebra
3.1

The product representation R descends exactly when R(hk)=R(h) for every hH,kK, equivalently when R(k)=I. In that case define π(p(h))=R(h); this is well defined and is a homomorphism. Local inverse sheets of the covering show it is continuous and smooth. Necessity follows by pulling back any representation of G. Step 2.1 proves the equivalent character-lattice condition. In the forward direction, the irreducibility established in step 1.1 means the nonzero highest vector of step 1.2 generates the whole derived-algebra module, not merely a submodule. If s=0, irreducibility forces dimension one, its derived highest weight is zero, and the independent datum is exactly a torus character. These arguments prove the Statement including the central-action qualification.

A1step 1.1step 1.2step 1.3step 2.1

Depends on

Used by

Dependency tree · two levels

67 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources