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 $Z$ is the circle

Example

The dual of the discrete additive group $Z$ (The integers as equivalence classes of pairs of naturals, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies) is canonically isomorphic to the multiplicative unit circle (The multiplicative unit circle is a compact metrizable topological abelian group): the map $z \mapsto γ_{z}$ with $γ_{z} (n) : = z^{n}$ is an isomorphism of topological groups $T \to \hat{Z}$ . Under the identification $T ≅ R / Z$ this reads $\hat{Z} ≅ R / Z$ .

Facts & Assumptions

[F1]

The dual $\hat{G}$ consists of the continuous homomorphisms $G \to T$ with pointwise multiplication and the compact-open topology; on a discrete domain the compact-open topology is the topology of pointwise convergence, i.e. the subspace topology from $T^{G}$ . (The Pontryagin dual with the compact-open topology, On a discrete domain the compact-open topology is the topology of pointwise convergence, The topology of pointwise convergence on $Y^{X}$ , which is the product topology, and its restriction to $C (X, Y)$ , Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace)

[F2]

$Z$ is discrete, so every function on $Z$ is continuous; integer powers in a group satisfy $z^{m + n} = z^{m} z^{n}$ and $z^{- n} = (z^{n})^{- 1}$ for $z \neq 0$ , and $(z w)^{n} = z^{n} w^{n}$ in an abelian group. (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Continuity of a map of topological spaces at a point and globally, 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, Integer powers in the complex field, Monoid homomorphism and group homomorphism)

[F3]

$T$ is a topological abelian group, so $z \mapsto z^{n}$ is continuous on $T$ for every $n$ ; a map into a product is continuous exactly when its components are, and composites of continuous maps are continuous. (The multiplicative unit circle is a compact metrizable topological abelian group, A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous)

[F4]

A bijective continuous homomorphism with continuous inverse is an isomorphism of topological groups. (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological)

Verification

Given: The discrete additive group $Z$ , the unit circle $T$ , and the map $Ψ (z) : = γ_{z}$ with $γ_{z} (n) = z^{n}$ .

1.1F1F2

For each $z \in T$ the map $γ_{z} : Z \to T$ , $γ_{z} (n) = z^{n}$ , is a character: it is a homomorphism by the power laws $γ_{z} (m + n) = z^{m + n} = z^{m} z^{n}$ of [F2], and it is continuous because for every open $V \subseteq T$ , $γ_{z}^{- 1} [V]$ is a subset of the discrete source $Z$ , hence open; at each point mapped into $V$ it is the source neighbourhood required by [F2].

1.2F1F3

The inverse $γ \mapsto γ (1)$ is continuous: it is the restriction to the subspace $\hat{Z}$ of the projection $π_{1} : T^{Z} \to T$ , which is continuous for the product topology by [F3], and a restriction of a continuous map to a subspace is continuous by the characteristic property of the subspace topology [F1].

2.1step 1.1F2

$Ψ$ is a bijective group homomorphism: it is a homomorphism because $γ_{z w} (n) = (z w)^{n} = z^{n} w^{n} = (γ_{z} γ_{w}) (n)$ by [F2]; it is injective because $γ_{z} (1) = z$ recovers $z$ ; and it is surjective because a homomorphism $γ$ determines $z : = γ (1)$ and then $γ (n) = z^{n}$ for $n \geq 0$ by induction and $γ (n) = γ (- n)^{- 1} = z^{n}$ for $n < 0$ by the power laws of [F2], so $γ = γ_{z}$ .

2.2step 1.1F1F3

$Ψ$ is continuous: the codomain carries the subspace topology from $T^{Z}$ by [F1], so by the characteristic property of the subspace it suffices that $z \mapsto (z^{n})_{n \in Z}$ is continuous into $T^{Z}$ , and by [F3] it suffices that each component $z \mapsto z^{n}$ is continuous, which holds because $T$ is a topological group by [F3].

3.1step 1.1step 1.2step 2.1step 2.2F4∎

By steps 1.1, 1.2, 2.1 and 2.2 the map $Ψ$ is a continuous bijective homomorphism with continuous inverse, hence an isomorphism of topological groups $T \to \hat{Z}$ by [F4]; composing with the topological group isomorphism $R / Z \to T$ gives $\hat{Z} ≅ R / Z$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

The Pontryagin dual of ZZ is the circle