TheoremStatement: 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.

The dual of a locally compact abelian group is locally compact abelian

Statement

Assume the Axiom of Choice (The Axiom of Choice). If $G$ is a locally compact Hausdorff abelian group (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space), then $\hat{G}$ is a locally compact Hausdorff abelian topological group, and the sets ${γ : γ [K] \subseteq V}$ with $K \subseteq G$ compact and $V \subseteq T$ open with $1 \in V$ form a basis of neighbourhoods of the identity character (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

Facts & Assumptions

[F1]

$\hat{G}$ is a Hausdorff topological abelian group, translations are homeomorphisms, and its topology is generated by the subbasis $S (K, V) = {γ : γ [K] \subseteq V}$ with $K \subseteq G$ compact and $V \subseteq T$ open. (The compact-open character group is a Hausdorff topological abelian group, The Pontryagin dual with the compact-open topology, The compact-open topology on $C (X, Y)$ for arbitrary topological spaces, Left and right translations and inversion in a topological group are homeomorphisms)

[F2]

Assume the Axiom of Choice. For every symmetric compact neighbourhood $K$ of $0$ in $G$ , the set $N_{K} : = {γ \in \hat{G} : γ [K] \subseteq D}$ with $D = {∣ z - 1 ∣ \leq 1 / 2}$ is equicontinuous, is compact in the compact-open topology of $C (G, T)$ , and is a neighbourhood of the identity character in $\hat{G}$ . (A compact identity neighbourhood in the dual, The Axiom of Choice)

[F3]

In a locally compact Hausdorff space every point has a compact neighbourhood, and we may take it symmetric in a topological group: if $N$ is a compact neighbourhood of $0$ then so is $N \cap (- N)$ . (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, In a locally compact Hausdorff space every open set containing a point contains an open set containing it whose closure is compact and still inside; such a space is regular, Left and right translations and inversion in a topological group are homeomorphisms, In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, 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)

[F4]

A composite of continuous maps is continuous. (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous)

Proof

Given: A locally compact Hausdorff abelian group $G$ , and $\hat{G}$ with the compact-open topology.

1.1F1

$\hat{G}$ is a Hausdorff abelian topological group by [F1].

1.2F1

The sets $S (K, V)$ with $K$ compact and $V$ open containing $1$ form a basis of neighbourhoods of $1$ in $\hat{G}$ : any open neighbourhood of $1$ contains a finite intersection $⋂_{i \leq n} S (K_{i}, V_{i})$ of subbasic sets each containing $1$ by [F1], and that intersection contains the subbasic set $S (⋃_{i \leq n} K_{i}, ⋂_{i \leq n} V_{i})$ , where the union of finitely many compact sets is compact, the finite intersection of open sets is open and contains $1$ , and $1 (K) = {1}$ lies in every $V$ with $1 \in V$ .

2.1step 1.1F1F2F3F4

$\hat{G}$ is locally compact: by [F3] choose a symmetric compact neighbourhood $K$ of $0$ in $G$ (a compact neighbourhood intersected with its inverse image under the continuous inversion is compact and symmetric). By [F2] the set $N_{K} = {γ : γ [K] \subseteq D}$ is a compact neighbourhood of $1$ in $\hat{G}$ ; translations are homeomorphisms of $\hat{G}$ by [F1], so every character has a compact neighbourhood, and $\hat{G}$ is locally compact by [F1].

3.1step 1.1step 1.2step 2.1∎

By steps 1.1, 1.2 and 2.1 the dual $\hat{G}$ is a locally compact Hausdorff abelian topological group and the compact-open sets $S (K, V)$ form a basis of neighbourhoods of the identity character, as asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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