CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Dualisation is a contravariant involution

Statement

Assume the Axiom of Choice (The Axiom of Choice) and Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $φ : G \to H$ be a continuous homomorphism of locally compact Hausdorff abelian groups. Then $\hat{φ} : \hat{H} \to \hat{G}$ , $\hat{φ} (γ) : = γ \circ φ$ , is a continuous homomorphism, $\hat{{id}_{G}} = {id}_{\hat{G}}$ , and for composable $φ, ψ$ one has $\hat{ψ \circ φ} = \hat{φ} \circ \hat{ψ}$ ; thus $(-)^{\land}$ is a contravariant functor into locally compact Hausdorff abelian groups. Moreover the evaluation maps are natural, $Φ_{H} \circ φ = \hat{\hat{φ}} \circ Φ_{G},$ so that $Φ$ is a natural isomorphism from the identity functor to the double-dual functor; dualisation is therefore a contravariant involution of the category of locally compact Hausdorff abelian groups, and it preserves finite products, closed subgroups and quotients in the sense of Biduality commutes with products, closed subgroups and quotients.

Facts & Assumptions

Given: Continuous homomorphisms $φ : G \to H$ , $ψ : H \to J$ of locally compact Hausdorff abelian groups.

[F1]

Pullback along a continuous homomorphism is a continuous group homomorphism; the dual of a locally compact Hausdorff abelian group is again locally compact Hausdorff and abelian; pullback carries identities to identities and reverses composition. (Dual homomorphisms: continuity, and the annihilator of a closed subgroup, The dual of a locally compact abelian group is locally compact abelian, The Pontryagin dual with the compact-open topology, Topological group: multiplication and inversion are continuous, Monoid homomorphism and group homomorphism, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological)

[F2]

For every locally compact Hausdorff abelian group $A$ the evaluation map $Φ_{A} (a) (λ) = λ (a)$ is an isomorphism of topological groups $A \to \hat{\hat{A}}$ . (Pontryagin biduality: the evaluation map is a topological isomorphism)

[F3]

Naturality of evaluation is the direct computation $Φ_{H} (φ (x)) (γ) = γ (φ (x)) = Φ_{G} (x) (γ \circ φ) = (\hat{\hat{φ}} (Φ_{G} (x))) (γ)$ for $x \in G$ , $γ \in \hat{H}$ . (The Pontryagin dual with the compact-open topology, Monoid homomorphism and group homomorphism)

[F4]

Biduality commutes with finite products, closed subgroups and quotients, with the evaluation isomorphisms intertwining the exact sequences. (Biduality commutes with products, closed subgroups and quotients)

Proof

1.1F1

Functoriality: $\hat{φ} (γ) = γ \circ φ$ is a continuous homomorphism by [F1]; $\hat{{i d}_{G}} (γ) = γ \circ {i d}_{G} = γ$ ; and for composable $ψ : H \to J$ one computes $\hat{ψ \circ φ} (γ) = γ \circ ψ \circ φ = \hat{φ} (\hat{ψ} (γ))$ , that is $\hat{ψ \circ φ} = \hat{φ} \circ \hat{ψ}$ .

1.2F3

Naturality: by the computation of [F3], $Φ_{H} \circ φ = \hat{\hat{φ}} \circ Φ_{G}$ for every continuous homomorphism $φ$ .

2.1F2F4step 1.1step 1.2∎

Since every $Φ_{A}$ is an isomorphism of topological groups by [F2] and the family is natural by step 1.2, $Φ$ is a natural isomorphism from the identity functor of the category of locally compact Hausdorff abelian groups to the double-dual functor; because $(-)^{\land}$ is contravariant by step 1.1 and $Φ$ is a natural isomorphism, dualisation is a contravariant involution. Its compatibility with finite products, closed subgroups and quotients is [F4], which also records that $H^{⊥ ⊥} = H$ for closed subgroups.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C (course-hosted full text) (standard reference, not scraped)