Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Characters are the integral weights

Statement

Assume the Axiom of Choice. Let T be a torus with Lie algebra t and exponential map exp:tT, normalized so that the exponential of the circle group satisfies exp(2πi)=1. Differentiation identifies the character lattice X(T) with the set {λHomC(tC,C): λ(Λ)2πiZ},Λ=kerexp, through the formula χ(expX)=eλ(X); the cocharacter lattice is identified with the lattice 12πΛ={Xt:2πXΛ} through η(eiθ)=exp(θXη), and under these identifications the pairing is χ,η=λ(Xη)iZ. In particular X(T) and X(T) are free abelian groups of rank dimT, and the pairing X(T)×X(T)Z is perfect.

Facts & Assumptions

Given: Assume the Axiom of Choice, a torus T with Lie algebra t and kernel Λ=kerexp.

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through the structure theorem [L1].

[L1]

exp:tT is surjective with kernel a full lattice Λ, and the induced map t/ΛT is a Lie-group isomorphism (Structure of compact connected abelian Lie groups).

[L2]

A character is a continuous homomorphism χ:TS1, a cocharacter a continuous homomorphism η:S1T, and the pairing is the integer n with χη(z)=zn (Character and cocharacter lattices).

[L3]

Every continuous homomorphism ψ:VS1 from a finite-dimensional real vector space has a unique form ψ(X)=eiμ(X) for some μV. Indeed, after choosing a basis it is enough to treat a continuous homomorphism u:RS1. A continuous argument a with a(0)=0 exists on a small interval. Whenever s,t,s+t lie in a sufficiently small interval, a(s+t)a(s)a(t) is a continuous 2πZ-valued function that vanishes at (0,0), hence is zero. The continuous local Cauchy equation gives a(t)=ct there, and for arbitrary t, choosing n with t/n in that interval gives u(t)=u(t/n)n=eict. Combining the coordinates proves existence; uniqueness follows by restricting to each basis line. A continuous homomorphism S1S1 has the form zzn for a unique nZ by Character and cocharacter lattices.

Proof

technique · direct
1.1

Let χX(T). The composite χexp:tS1 is a continuous homomorphism, so [L3] gives a unique μt with χ(expX)=eiμ(X). Put λ=iμ and extend it C-linearly to tC. If YΛ, then 1=χ(expY)=eλ(Y), so λ(Y)2πiZ; the map χλ is injective because exp is surjective.

L1L2L3
1.2

Choose a Z-basis Y1,,Yr of the full lattice Λ. By [L1], Φ:(S1)rT,qquadΦ(eiθ1,,eiθr)=exp ⁣(j=1rθj2πYj) is a Lie-group isomorphism. If η:S1T is a cocharacter, each coordinate of Φ1η is zznj for a unique njZ by [L3]. Thus, with Xη=j=1rnj2πYj, one has η(eiθ)=exp(θXη) and 2πXηΛ. Conversely every Xt with 2πXΛ gives the well-defined cocharacter eiθexp(θX). Hence X(T) is identified with 12πΛ, and the displayed formula also shows that Xη=dη1(i).

L1L2L3
2.1

Conversely let λHomC(tC,C) satisfy λ(Λ)2πiZ. Since the lattice basis in step 1.2 spans t over R, the restriction of λ to t takes values in iR. Therefore χ(expX):=eλ(X) takes values in S1 and is well defined: if expX=expX then XXΛ, so eλ(XX)=1. It is a continuous homomorphism TS1, so it is a character, and its differentiated weight is λ; hence the constructions are mutually inverse bijections.

L1L2step 1.1step 1.2
2.2

Pairing: with χ and λ related as in step 1.1 and η with 2πXηΛ as in step 1.2, one has χ(η(eiθ))=eλ(θXη)=eiθλ(Xη)/i, so the integer n with χη(z)=zn is n=λ(Xη)/i; it is an integer because 2πXηΛ and λ(2πXη)2πiZ, so that λ(Xη)/i=λ(2πXη)/(2πi)Z.

L1L2step 1.1step 1.2
3.1

Perfectness and freeness: choosing a Z-basis Y1,,Yr of Λ identifies ΛZr, hence also X(T)12πΛZr, while the characters correspond to the dual basis: λ is determined by the integers λ(Yj)/(2πi), and conversely every integer vector gives such a λ by linear extension, because the basis spans t over R. Hence X(T)Zr is free of rank r=dimT, the pairing is the dot product in these coordinates, and it is perfect.

A1L1step 2.1step 1.2step 2.2

Depends on

Used by

Dependency tree · two levels

11 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