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.

Structure of compact connected abelian Lie groups

Statement

Assume the Axiom of Choice. Let T be a compact connected abelian Lie group with Lie algebra t and exponential map exp:tT (Tori and maximal tori, Exponential map of a Lie group). Then exp is surjective, its kernel Λ=kerexp is a discrete full lattice in t, and T is isomorphic as a Lie group to t/Λ and to (S1)r, where r=dimt.

The cited torus definition supplies terminology only. The product-of-circles classification is not a premise here; it is the conclusion proved below.

Facts & Assumptions

Given: The Axiom of Choice and a compact connected abelian Lie group T with Lie algebra t and exponential map exp.

[A1]

The Axiom of Choice supplies the Axiom of Countable Choice ACω used by the exponential-map suppliers below (The Axiom of Choice, AC supplies the countable and dependent choices used in Banach integration).

[L1]

Under ACω, for commuting X,Yt one has exp(X+Y)=exp(X)exp(Y); in particular exp:tT is a homomorphism of abelian groups because t is abelian and T is abelian (Commuting Lie-algebra elements have multiplicative exponentials, Exponential map of a Lie group).

[L2]

Under ACω, the exponential map of a finite-dimensional real Lie group is a local diffeomorphism at 0: there are open neighbourhoods U of 0 in t and V of e in T such that expU:UV is a diffeomorphism; in particular kerexpU={0} (The exponential map is a local diffeomorphism at zero, Exponential map of a Lie group).

[L3]

Under ACω, R/Z carries the quotient topology and is homeomorphic to the circle. We write S1=R/Z as on this page; its quotient Lie-group structure and the smooth finite-product identification are constructed in steps 3.1 and 5.1 (The one-dimensional torus and its normalized Haar integral).

[L4]

A discrete subgroup of the additive group of a finite-dimensional real vector space V is a free abelian group, its rank equals the dimension of its real span, and it admits a Z-basis that is an R-basis of that span. (Proved internally in step 3.2, not assumed there.)

Proof

technique · direct
1.1

By [A1], the countable-choice hypotheses of [L1] and [L2] hold. The exponential map of an abelian Lie group is therefore a homomorphism by [L1], and by [L2] it maps the open neighbourhood U of 0 diffeomorphically onto the open neighbourhood V of e. Hence exp(t) contains V, and since exp(t) is a subgroup containing a neighbourhood of the identity, it is open; an open subgroup of a topological group is closed and its cosets partition the group, so connectedness of T forces exp(t)=T, that is, exp is surjective.

A1L1L2
2.1

The kernel Λ=exp1(e) is a subgroup of t and is discrete: by [L2], if ΛU contained a nonzero point then U would contain two distinct points with the same image under the diffeomorphism expU. It is closed in t as the preimage of the closed singleton {e} under the continuous map exp.

L2step 1.1
3.1

Construct the smooth quotient explicitly. For a closed discrete subgroup D of a finite-dimensional real vector space E, the quotient map q:EE/D is open, since q1(q(O))=dD(O+d) for open O. Choose a ball B about 0 with (BB)D={0}. The restrictions of q to translates of B are homeomorphisms onto open sets and supply coordinate charts. On overlaps, the two lifts differ locally by a fixed element of D, so chart transitions are translations and are smooth. Distinct cosets have disjoint small chart neighbourhoods: if xyD, closedness of D gives a ball about xy disjoint from D. Images of a countable Euclidean base give a countable base for the quotient. Thus these charts define a Hausdorff, second-countable smooth manifold, and addition and inversion are smooth, being locally addition and negation followed by translations. This is the unique smooth structure for which q is a local diffeomorphism. Apply the construction to E=t and D=Λ. The map expˉ:t/ΛT, X+ΛexpX, is a well-defined bijective homomorphism by steps 1.1 and 2.1. Shrink B into the neighbourhood U of [L2]. In the resulting quotient chart, expˉ is exactly expB, hence a local diffeomorphism; translations give this property everywhere. A bijective local diffeomorphism has smooth local inverses that form its global inverse. Therefore expˉ is a Lie-group isomorphism.

L1L2step 1.1step 2.1construct
3.2

The kernel Λ is a lattice in its real span. We prove the lattice assertion by induction; when the span is zero the subgroup is {0} with the empty basis. If V:=span(Λ) is nonzero, fix a Euclidean norm and choose X1Λ{0} of least norm; such an element exists because a closed discrete subset meets every compact ball in a finite set. Subtracting a nearest integer multiple of X1 shows ΛRX1=ZX1. Let p:VX1 be orthogonal projection. For each XΛ, subtract an integer multiple of X1 so that the X1-coordinate lies in [1/2,1/2]. The resulting representatives with p(X)1 lie in a compact cylinder, whose intersection with Λ is finite. If that finite set has nonzero projected norms, their minimum is positive; otherwise p(Λ) has no nonzero point of norm at most 1. In either case 0 is isolated in p(Λ), and translation makes p(Λ) discrete. Such a subgroup is also closed: near any point in its closure a ball of diameter smaller than its positive separation contains at most one subgroup point, forcing the limit to equal that point. Induction on dimV gives a Z-basis of p(Λ) whose lifts X2,,XmΛ, together with X1, generate Λ and are linearly independent over R. Thus Λ is free abelian of rank m=dimV with a Z-basis that is an R-basis of V.

step 2.1construct
4.1

The rank equals n:=dimt: if V=span(Λ)t, then the map X+ΛX+V is well defined and continuous by the quotient topology and gives a surjection t/Λt/VRnm with nm>0; its image is compact by [L5], while Rnm is not compact, a contradiction. Hence m=n, so Λ has a Z-basis X1,,Xn that is an R-basis of t; in particular Λ is a full lattice and Tt/Λ by step 3.1.

L4L5step 3.1step 3.2
5.1

The linear isomorphism Rnt, (a1,,an)iaiXi, carries Zn onto Λ. In the quotient charts of step 3.1 it and its inverse remain smooth, so it induces a Lie-group isomorphism Rn/Znt/Λ. By [A1] the countable-choice hypothesis of [L3] holds. Equip S1=R/Z with the quotient charts of step 3.1, using open intervals of length less than 1. The coordinate map [a1,,an]([a1],,[an]) is a bijective homomorphism from Rn/Zn to (S1)n. On products of these intervals its coordinate expression and inverse are the identity, so it is a Lie-group isomorphism for the product smooth structure. Composing gives T(S1)r with r=n. If n=0, surjectivity of exp:{0}T gives T={e}, Λ={0}, and the same conclusion uses the empty product. No choice beyond [A1] is required by the finite lattice construction or quotient charts.

A1L3step 3.1step 4.1

Depends on

Used by

Dependency tree · two levels

83 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