LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Continuous characters of the real line are exponentials

Statement

Every continuous group homomorphism $φ : R \to T$ from the additive line to the multiplicative unit circle (The multiplicative unit circle is a compact metrizable topological abelian group) is $φ (t) = \exp (2 π i ξ t)$ for a unique $ξ \in R$ ; conversely every such map $φ_{ξ} (t) = \exp (2 π i ξ t)$ is a continuous character of the additive line.

Facts & Assumptions

[F1]

$ε : R / Z \to T$ , $ε ([t]) = \exp (2 π i t)$ , is an isomorphism of topological groups; in particular $ε$ and its inverse are continuous, $ε ([0]) = 1$ , and $ε ([t])$ has modulus $1$ for every real $t$ . (The multiplicative unit circle is a compact metrizable topological abelian group)

[F2]

$p : R \to R / Z$ , $p (t) = [t]$ , is a covering map, it is the quotient homomorphism of the additive group $R$ modulo $Z$ , so $p (u + v) = p (u) + p (v)$ , and $p (u) = [0]$ exactly when $u \in Z$ . ( $p : R \to R / Z$ is a covering map with translated interval sheets, The one-dimensional torus and its normalized Haar integral)

[F3]

$R$ is path-connected and locally path-connected, and it is simply connected: its fundamental group at $0$ is trivial. ( $R^{n}$ is polygonally connected, connected, locally path-connected and locally connected, Every nonempty convex subset of $R^{n}$ is simply connected, Simply connected topological spaces, Paths, path-connected spaces and path components)

[F4]

Lifting criterion: for a path-connected and locally path-connected $Y$ , a based map $f : (Y, y_{0}) \to (B, b_{0})$ and a covering $p : (E, e_{0}) \to (B, b_{0})$ , a based lift of $f$ exists if and only if $f_{*} π_{1} (Y, y_{0}) \subseteq p_{*} π_{1} (E, e_{0})$ , and it is unique. (Lifting criterion for maps from path-connected locally path-connected spaces, Lifts of maps, paths, and homotopies through a covering map)

[F5]

The continuous image of a connected space is connected, and a connected subset of $R$ is order-convex. (A continuous image of a connected space is connected, and connectedness is a topological property, The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ ", Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets)

[F6]

An additive function $f : R \to R$ that is continuous at a single point satisfies $f (x) = f (1) x$ for every real $x$ . (Six regularity conditions each force an additive $f : R \to R$ to be $x \mapsto f (1) x$ : continuity at a single point, monotonicity on a nondegenerate interval, boundedness above on one, boundedness below on one, constancy of sign on one, and a graph that is not dense in $R^{2}$ )

[F7]

$\exp (z + w) = \exp z \exp w$ for complex $z, w$ ; $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , so $∣ \exp (i y) ∣ = 1$ and $\exp (0) = 1$ ; and $e^{i π} + 1 = 0$ . ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The complex exponential by its power series)

[F8]

Composites of continuous maps are continuous, and the identity together with its real scalar multiples $t \mapsto ξ t$ are continuous. (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function)

Proof

Given: A continuous group homomorphism $φ : R \to T$ of the additive line.

1.1F1F3F8

The map $ψ : = ε^{- 1} \circ φ : R \to R / Z$ is a continuous group homomorphism with $ψ (0) = [0]$ : $ε^{- 1}$ is continuous by [F1], $R$ is path-connected by [F3], and $ψ (0) = ε^{- 1} (φ (0)) = ε^{- 1} (1) = [0]$ because a group homomorphism sends the identity to the identity (Monoid homomorphism and group homomorphism) and $ε ([0]) = 1$ by [F1].

2.1step 1.1F2F3F4

There is a continuous lift $θ : R \to R$ with $p \circ θ = ψ$ and $θ (0) = 0$ : the domain $R$ is path-connected and locally path-connected and its fundamental group at $0$ is trivial by [F3], so $ψ_{*} π_{1} (R, 0) \subseteq p_{*} π_{1} (R, 0)$ holds vacuously, and the lifting criterion [F4] applied to $ψ$ and the covering $p$ of [F2] supplies the based lift.

3.1step 1.1step 2.1F2F8

For fixed real $t$ the map $h (s) : = θ (s + t) - θ (s) - θ (t)$ is continuous and takes values in $Z$ : continuity is by [F8], and $p (θ (s + t)) = ψ (s + t) = ψ (s) + ψ (t) = p (θ (s)) + p (θ (t)) = p (θ (s) + θ (t))$ by [F2] and step 1.1, so $θ (s + t) - θ (s) - θ (t) \in \ker p = Z$ by [F2].

4.1step 2.1step 3.1F5

The image $h [R]$ is connected by [F5], being the continuous image of the connected space $R$ ; being a connected subset of $R$ it is order-convex by [F5], and an order-convex subset of $Z$ with two distinct elements $a < b$ would contain $a + 1 / 2 \notin Z$ , so $h [R]$ is a singleton. Since $h (0) = θ (t) - θ (0) - θ (t) = 0$ by step 2.1, that singleton is ${0}$ , so $θ (s + t) = θ (s) + θ (t)$ for all real $s, t$ : the lift $θ$ is additive.

5.1step 2.1step 4.1F6

By steps 2.1 and 4.1 the map $θ$ is additive and continuous, hence $θ (t) = ξ t$ for every real $t$ , where $ξ : = θ (1)$ , by [F6].

6.1step 2.1step 5.1F1F2

Consequently $φ (t) = ε (ψ (t)) = ε (p (θ (t))) = ε ([θ (t)]) = \exp (2 π i θ (t)) = \exp (2 π i ξ t)$ for every real $t$ , by [F1], [F2], step 2.1 and step 5.1.

7.1step 6.1F7

The parameter $ξ$ is unique: if $\exp (2 π i ξ t) = \exp (2 π i ξ^{'} t)$ for all real $t$ , then $\exp (2 π i (ξ - ξ^{'}) t) = 1$ for all $t$ by [F7]; were $ξ \neq ξ^{'}$ , the choice $t = 1 / (2 ∣ ξ - ξ^{'} ∣) > 0$ would give $\exp (\pm π i) = - 1$ by [F7], contradicting $\exp (\pm π i) = 1$ ; hence $ξ = ξ^{'}$ .

8.1step 6.1F1F2F7F8∎

Conversely, for every real $ξ$ the map $φ_{ξ} (t) : = \exp (2 π i ξ t)$ is a continuous group homomorphism $R \to T$ : it is a homomorphism by the addition formula [F7], it takes values in $T$ because $∣ \exp (2 π i ξ t) ∣ = 1$ by [F7], and it is the composite $ε \circ p \circ (t \mapsto ξ t)$ of the continuous maps $t \mapsto ξ t$ [F8], $p$ [F2] and $ε$ [F1], hence continuous by [F8].

Depends on

Used by

Dependency tree · two levels

155 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

Dikran D. Dikranjan, Introduction to Topological Groups (author lecture notes, Universita di Udine / Universidad Complutense de Madrid, 2007) (standard reference, not scraped)
Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C (course-hosted full text) (standard reference, not scraped)
Lynn H. Loomis, Introduction to Abstract Harmonic Analysis, D. Van Nostrand 1953, Chapter VII, Sections 34-35 (printed pp. 134-140) (standard reference, not scraped)