ExampleConstruction: Literature-sourcedVerification: 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.

The Pontryagin dual of a finite cyclic group

Example

For $N \geq 1$ , on the presented group $Z / N Z$ carrying the quotient topology of the discrete group $Z$ (so that the finite group is discrete), every continuous homomorphism $χ : Z / N Z \to T$ is $χ ([m]) = \exp (2 π i k m / N)$ for a unique $k \in Z / N Z$ , and $k \mapsto χ_{k}$ is an isomorphism of topological groups $Z / N Z \to \hat{Z / N Z}$ for the presented group (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold); no generator of an abstract cyclic group is chosen.

Facts & Assumptions

[F1]

The dual consists of the continuous homomorphisms into $T$ with pointwise multiplication and the compact-open topology; a finite group is compact in the discrete topology and its dual is discrete. (The Pontryagin dual with the compact-open topology, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Compact groups have discrete duals and discrete groups have compact duals)

[F2]

In the presented group $Z / N Z$ one has $N [1] = [0]$ and $[m] = m [1]$ , and $[m] = [m^{'}]$ holds exactly when $m \equiv m^{'} (m o d N)$ . (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold)

[F3]

The $N$ -th roots of unity in $T$ are exactly the numbers $\exp (2 π i k / N)$ with $k \in Z$ , and $\exp (2 π i k / N) = \exp (2 π i k^{'} / N)$ holds exactly when $k \equiv k^{'} (m o d N)$ ; the identity $\exp (2 π i u) = 1$ for real $u$ holds exactly when $u \in Z$ . (The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The zero sets of sine and cosine and the least positive common period 2 pi)

[F4]

The addition formula $\exp (u + v) = \exp u \exp v$ gives $\exp (m z) = (\exp z)^{m}$ for integers $m$ by induction and inversion. $T$ is a topological abelian group and group powers satisfy $z^{m + n} = z^{m} z^{n}$ ; a bijection between discrete spaces is a homeomorphism. ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, The multiplicative unit circle is a compact metrizable topological abelian group, Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies)

Verification

Given: $N \geq 1$ , the presented group $Z / N Z$ , and the unit circle $T$ .

1.1F2F3F4

Let $χ$ be a continuous homomorphism of $Z / N Z$ into $T$ and put $ζ : = χ ([1])$ . Then $ζ^{N} = χ ([1])^{N} = χ (N [1]) = χ ([0]) = 1$ by [F2] and the power laws of [F4], so $ζ$ is an $N$ -th root of unity and by [F3] there is $k \in Z$ with $ζ = \exp (2 π i k / N)$ ; then $χ ([m]) = χ ([1])^{m} = \exp (2 π i k m / N)$ for every $m$ by [F2] and the power laws.

2.1step 1.1F1F2F3F4

The integer $k$ is unique modulo $N$ , and every $k$ defines a character: if $\exp (2 π i k m / N) = \exp (2 π i k^{'} m / N)$ for all $m$ , then for $m = 1$ the congruence $k \equiv k^{'} (m o d N)$ follows from [F3]; conversely for fixed $k$ the formula $χ_{k} ([m]) : = \exp (2 π i k m / N)$ is well defined by [F3] and [F2], is a homomorphism because $\exp (2 π i k (m + m^{'}) / N) = \exp (2 π i k m / N) \exp (2 π i k m^{'} / N)$ , and is continuous because $Z / N Z$ is finite and discrete by [F1].

3.1step 1.1step 2.1F3F4

The map $k \mapsto χ_{k}$ from $Z / N Z$ to the dual is a bijective homomorphism: $χ_{k + k^{'}} = χ_{k} χ_{k^{'}}$ by the addition formula, injectivity is step 2.1, and surjectivity is step 1.1 combined with the uniqueness in step 2.1.

4.1step 3.1F1F4∎

It is a homeomorphism: $Z / N Z$ is finite and discrete by [F1], its dual is discrete by [F1] because the finite discrete group is compact, and any bijection between discrete spaces is a homeomorphism by [F4]; hence $k \mapsto χ_{k}$ is an isomorphism of topological groups.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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