Alphabeta Math
TheoremStatement: 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.

Conjugacy of maximal tori

Statement

Assume the Axiom of Choice. Any two maximal tori of a compact connected Lie group are conjugate.

Facts & Assumptions

Given: AC, a compact connected Lie group G, and maximal tori T1,T2 with Lie algebras t1,t2g.

[A1]

AC is The Axiom of Choice; it supplies the metric existence theorem and countable choice for the Lie-group interfaces below.

[L1]

A compact Lie group admits a bi-invariant metric (Compact Lie groups admit bi-invariant metrics). The adjoint map is a smooth homomorphism (Adjoint is a smooth Lie-group representation), defined as the differential of conjugation (Conjugation and the adjoint representation of a Lie group), with dAde(X)(U)=[X,U] (The differential of Ad is ad).

[L2]

A torus of G is a compact connected abelian closed embedded Lie subgroup, and maximal means maximal by inclusion (Tori and maximal tori). A closed subgroup of a Lie group is embedded (Cartan closed subgroup theorem). Closure preserves connectedness (If A is connected and ABA then B is connected; in particular the closure of a connected set is connected), and closed subsets of a compact space are compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[L3]

For commuting Lie-algebra elements, exp(U+V)=expUexpV=expVexpU (Commuting Lie-algebra elements have multiplicative exponentials). The exponential is locally a diffeomorphism at zero (The exponential map is a local diffeomorphism at zero) and is natural for homomorphisms (Exponential map is natural for Lie-group homomorphisms). Also texp(tV) has initial velocity V (Exponential scales one-parameter subgroups).

[L4]

A normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely). A commuting family of diagonalizable endomorphisms is simultaneously diagonalizable (A family of diagonalisable endomorphisms of a finite-dimensional space is simultaneously diagonalisable if and only if its members commute pairwise).

[L5]

A finite-dimensional vector space over an infinite field is not a finite union of proper linear subspaces (A finite-dimensional vector space over an infinite field is not a finite union of proper subspaces).

[L6]

Connected immersed Lie subgroups are uniquely determined, as subgroups with their intrinsic smooth structures, by their Lie subalgebras (Lie subgroup–Lie subalgebra correspondence).

Proof

technique · direct
1.1

Choose the metric of [L1] and its inner product on g. Conjugation is a composite of left and right isometries fixing e, so its differential Adg preserves this inner product. Differentiate along exp(tX) using [L1] and [L3] to obtain [X,U],V=U,[X,V]. Thus every adX is skew-adjoint.

A1L1L3
1.2

If an abelian Lie subalgebra a contains ti, then A=expG(a) is a subgroup by [L3] and is abelian; it is connected as the continuous image of a vector space. Its closure H is a connected compact subgroup by [L2]. To check the group and abelian assertions for the closure, continuity of multiplication, inversion and the commutator map extends the corresponding identities from the dense subset A (and A×A) to H (and H×H). The closed-subgroup theorem gives its embedded Lie structure. For Va, the curve expG(tV) lies in H, and submanifold charts make this ambient smooth curve smooth as an H-valued curve; hence its velocity V lies in LieH. Naturality and local invertibility of the exponential on Ti show that A contains an identity neighborhood in Ti; the subgroup it generates is open and closed in connected Ti, hence is all of Ti. Thus H is a torus containing Ti, so maximality gives H=Ti and ati. Therefore ti is maximal abelian.

L2L3
2.1

Fix either t=ti. Extend the real inner product to the positive Hermitian product on gC using a real orthonormal basis. The operators adH, Ht, remain skew-adjoint after complexification, so are normal and diagonalizable by [L4]. They commute because [H,H]=0 and Jacobi gives [adH,adH]=ad[H,H]. Simultaneous diagonalization yields finitely many joint eigenspaces with eigenvalue functions α:tC that are real-linear, by linearity of HadH. The joint zero eigenspace is tC: if a real U commutes with all of t, then t+RU is abelian, so Ut by step 1.2; for complex U the real and imaginary parts separately commute.

L4step 1.1step 1.2algebra
3.1

For every nonzero eigenvalue function α in step 2.1, its real kernel is a proper subspace of t. By [L5] choose Xi outside the finite union of these kernels. On each nonzero joint eigenspace adXi has nonzero eigenvalue, and its kernel is therefore exactly ti,C. Intersecting with g gives cg(Xi)=ti. If the family of nonzero eigenvalue functions is empty, step 2.1 says ti=g, and Xi=0 works, including the zero-dimensional case.

L5step 2.1
4.1

Put X=X1 and Y=X2. The smooth function f(g)=AdgX,Y attains a maximum at g0 by compactness. For each Zg, differentiate f(exp(tZ)g0) at zero. With U=Adg0X, the derivative is [Z,U],Y=Z,[U,Y] by step 1.1 and symmetry. Its vanishing for every Z implies [U,Y]=0.

L1L3step 1.1step 3.1
5.1

Step 3.1 gives Uc(Y)=t2. Since t2 is abelian, t2c(U)=Adg0c(X)=Adg0t1. The last space is abelian because conjugation induces a Lie-algebra automorphism. Maximal abelianness of t2 forces equality.

L1step 1.2step 3.1step 4.1
6.1

The connected embedded subgroups g0T1g01 and T2 have the same Lie algebra by step 5.1, and therefore are the same subgroup by [L6]. This proves conjugacy. The argument includes trivial tori, the zero Lie algebra and the empty family of nonzero weights as treated in step 3.1. All choice requirements are covered by [A1]; no reductivity, Cartan-subalgebra recognition, root decomposition or torus lattice classification was invoked.

A1L6step 3.1step 5.1

Depends on

Used by

Dependency tree · two levels

95 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