ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated

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.

The Pontryagin dual of Euclidean space is Euclidean space

Example

For $n \geq 1$ every continuous group homomorphism $φ : R^{n} \to T$ is $φ (x) = \exp (2 π i ξ \cdot x)$ for a unique $ξ \in R^{n}$ , and $ξ \mapsto φ_{ξ}$ is an isomorphism of topological groups $R^{n} \to \hat{R^{n}}$ (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

Facts & Assumptions

[F1]

Every continuous group homomorphism $ψ : R \to T$ is $ψ (t) = \exp (2 π i ξ t)$ for a unique $ξ \in R$ , and conversely each such map is a continuous character. (Continuous characters of the real line are exponentials)

[F2]

Coordinates of $R^{n}$ are indexed by $j < n$ . With the standard vectors $e_{j}$ one has $x = \sum_{j < n} x_{j} e_{j}$ and $ξ \cdot x : = \sum_{j < n} ξ_{j} x_{j}$ . Repeated application of the homomorphism law gives $φ (x) = \prod_{j < n} φ (x_{j} e_{j})$ . The coordinate inclusion $t \mapsto t e_{j}$ is continuous, since $d_{2} (t e_{j}, s e_{j}) = ∣ t - s ∣$ . (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Monoid homomorphism and group homomorphism)

[F3]

The circle has continuous multiplication and inversion. $\exp (u + v) = \exp u \exp v$ , so $\exp (2 π i (ξ + ξ^{'}) \cdot x) = \exp (2 π i ξ \cdot x) \exp (2 π i ξ^{'} \cdot x)$ , and $e^{i π} + 1 = 0$ . Moreover $u \mapsto \exp (2 π i u)$ is continuous at $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 multiplicative unit circle is a compact metrizable topological abelian group, Continuous characters of the real line are exponentials, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous)

[F4]

The product topology on $R^{n}$ is its Euclidean metric topology. Closed balls in $R^{n}$ are compact, and a continuous real-valued function on a nonempty compact set attains its maximum. (A subset of $R^{n}$ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane)

[F5]

The dual of a topological group is a Hausdorff topological group, so translations of the dual are homeomorphisms, and its compact-open subbasis is $S (K, W) = {γ : γ [K] \subseteq W}$ . Continuity of a homomorphism at the identity implies continuity everywhere by translating target neighbourhoods to the identity and translating the resulting source neighbourhoods back; translations in $R^{n}$ are isometries for $d_{2}$ and translations in the dual are homeomorphisms. (The compact-open character group is a Hausdorff topological abelian group, The Pontryagin dual with the compact-open topology, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it)

[F6]

On the nonempty compact subsets of a Euclidean space the quantity $R : = \max_{x \in K} ∥ x ∥_{2}$ is finite and $∣ ξ \cdot x ∣ \leq ∥ ξ ∥_{2} ∥ x ∥_{2}$ for all $x$ . The norm is continuous by $∣ ∥ x ∥_{2} - ∥ y ∥_{2} ∣ \leq ∥ x - y ∥_{2}$ . (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism)

Verification

Given: $n \geq 1$ and a continuous group homomorphism $φ : R^{n} \to T$ , together with the maps $φ_{ξ} (x) = \exp (2 π i ξ \cdot x)$ .

1.1F1F2F3

For each $j < n$ the map $ψ_{j} (t) : = φ (t e_{j})$ is a continuous group homomorphism $R \to T$ , so by [F1] there is a unique $ξ_{j} \in R$ with $ψ_{j} (t) = \exp (2 π i ξ_{j} t)$ . Define $ξ \in R^{n}$ by $ξ (j) : = ξ_{j}$ for $j < n$ . Consequently $φ (x) = \prod_{j < n} ψ_{j} (x_{j}) = \prod_{j < n} \exp (2 π i ξ_{j} x_{j}) = \exp (2 π i \sum_{j < n} ξ_{j} x_{j}) = \exp (2 π i ξ \cdot x)$ by [F2] and [F3].

2.1step 1.1F1

The vector $ξ$ is unique: if $\exp (2 π i ξ \cdot x) = \exp (2 π i ξ^{'} \cdot x)$ for all $x$ , then restricting to $x = t e_{j}$ for $j < n$ shows $ψ_{j} (t) = \exp (2 π i ξ_{j}^{'} t)$ , so the uniqueness in [F1] gives $ξ_{j} = ξ_{j}^{'}$ for every $j < n$ and hence $ξ = ξ^{'}$ .

3.1step 1.1step 2.1F1F2F3F5

Each $φ_{ξ}$ is a continuous character: it is the product over $j < n$ of the one-dimensional characters $x \mapsto \exp (2 π i ξ_{j} x_{j})$ composed with the continuous coordinate projections, so it is continuous, and the addition formula gives its homomorphism law. The map $ξ \mapsto φ_{ξ}$ is a bijective homomorphism: it is a homomorphism by [F3], injective by step 2.1, and surjective by step 1.1.

3.2step 2.1F3F5F6

It is continuous at the identity: let $K \subseteq R^{n}$ be compact and $W \subseteq T$ open with $1 \in W$ . If $K = \emptyset$ , $S (K, W)$ is the whole dual and there is nothing to check; otherwise choose $ρ > 0$ with $B (1, ρ) \subseteq W$ , and by continuity of $u \mapsto \exp (2 π i u)$ at $0$ by [F3] choose $δ^{'} > 0$ with $∣ \exp (2 π i u) - 1 ∣ < ρ$ whenever $∣ u ∣ < δ^{'}$ . With $R : = \max_{x \in K} ∥ x ∥_{2}$ by [F6], put $δ : = δ^{'} / (R + 1)$ ; if $∥ η ∥_{2} < δ$ and $x \in K$ , then $∣ η \cdot x ∣ \leq ∥ η ∥_{2} ∥ x ∥_{2} < δ^{'}$ , so $∣ φ_{η} (x) - 1 ∣ < ρ$ and $φ_{η} [K] \subseteq B (1, ρ) \subseteq W$ , that is $φ_{η} \in S (K, W)$ . Hence the map is continuous at the identity character and, being a homomorphism, continuous everywhere by [F5].

3.3step 2.1F3F4F5

It has continuous inverse: given $ε > 0$ , let $R : = 1 / (2 ε)$ and let $K$ be the closed ball of radius $R$ , compact by [F4]. If $φ_{η} \in S (K, B (1, 1))$ and $∥ η ∥_{2} \geq ε$ , then $x_{0} : = η / (2 ∥ η ∥_{2}^{2})$ satisfies $∥ x_{0} ∥_{2} = 1 / (2 ∥ η ∥_{2}) \leq R$ , so $x_{0} \in K$ , and $η \cdot x_{0} = 1 / 2$ , whence $∣ φ_{η} (x_{0}) - 1 ∣ = ∣ \exp (π i) - 1 ∣ = 2$ , contradicting $φ_{η} \in S (K, B (1, 1))$ ; therefore $∥ η ∥_{2} < ε$ . So the inverse map sends the identity neighbourhood $S (K, B (1, 1))$ into the ball of radius $ε$ , and it is continuous at the identity, hence everywhere by [F5].

4.1step 1.1step 2.1step 3.1step 3.2step 3.3∎

By steps 3.1, 3.2 and 3.3 the map $ξ \mapsto φ_{ξ}$ is a continuous bijective homomorphism with continuous inverse, hence an isomorphism of topological groups $R^{n} \to \hat{R^{n}}$ , and step 1.1 with step 2.1 is the stated classification with its uniqueness.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

154 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)
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)