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⁡:t→T, normalized so that the exponential of the circle group satisfies exp⁡(2πi)=1. Differentiation identifies the character lattice X∗(T) with the set {λ∈Hom⁡C(tC,C): λ(Λ)⊆2πi Z},Λ=ker⁡exp⁡, through the formula χ(exp⁡X)=eλ(X); the cocharacter lattice is identified with the lattice 12πΛ={X∈t:2πX∈Λ} through η(eiθ)=exp⁡(θXη), and under these identifications the pairing is ⟨χ,η⟩=λ(Xη)i∈Z. In particular X∗(T) and X∗(T) are free abelian groups of rank dim⁡T, 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 Λ=ker⁡exp⁡.

[A1]

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

[L1]

exp⁡:t→T 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 χ:T→S1, a cocharacter a continuous homomorphism η:S1→T, and the pairing is the integer n with χ∘η(z)=zn (Character and cocharacter lattices).

[L3]

Every continuous homomorphism ψ:V→S1 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:R→S1. 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 S1→S1 has the form z↦zn for a unique n∈Z by Character and cocharacter lattices.

Proof

technique · direct
1.1L1L2L3

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

1.2L1L2L3

Choose a Z-basis Y1,…,Yr of the full lattice Λ. By [L1], Φ:(S1)r⟶T,qquadΦ(eiθ1,…,eiθr)=exp⁡ ⁣(∑j=1rθj2πYj) is a Lie-group isomorphism. If η:S1→T is a cocharacter, each coordinate of Φ−1η is z↦znj for a unique nj∈Z by [L3]. Thus, with Xη=∑j=1rnj2πYj, one has η(eiθ)=exp⁡(θXη) and 2πXη∈Λ. Conversely every X∈t 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).

2.1L1L2step 1.1step 1.2

Conversely let λ∈Hom⁡C(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 χ(exp⁡X):=eλ(X) takes values in S1 and is well defined: if exp⁡X=exp⁡X′ then X−X′∈Λ, so eλ(X−X′)=1. It is a continuous homomorphism T→S1, so it is a character, and its differentiated weight is λ; hence the constructions are mutually inverse bijections.

2.2L1L2step 1.1step 1.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.

3.1A1L1step 2.1step 1.2step 2.2∎

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=dim⁡T, the pairing is the dot product in these coordinates, and it is perfect.

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