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

Biduality commutes with products, closed subgroups and quotients

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

(1) For locally compact Hausdorff abelian groups $G_{1}, \dots, G_{n}$ , under the product-dual identification $\hat{G_{1} \times \dots \times G_{n}} ≅ {\hat{G}}_{1} \times \dots \times {\hat{G}}_{n}$ of Duals of finite products and of discrete direct sums one has $Φ_{G_{1} \times \dots \times G_{n}} = Φ_{G_{1}} \times \dots \times Φ_{G_{n}}$ .

(2) For a closed subgroup $H \leq G$ of a locally compact Hausdorff abelian group $G$ , the evaluation isomorphisms intertwine the exact sequences $0 \to H \to G \to G / H \to 0$ with their duals: under the identifications $\hat{H} ≅ \hat{G} / H^{⊥}$ and $\hat{G / H} ≅ H^{⊥}$ of The dual of a closed subgroup is a quotient of the dual and The dual of a quotient is the annihilator, the restrictions of $Φ_{G}$ recover $Φ_{H}$ and $Φ_{G / H}$ , and $H^{⊥ ⊥} = H$ .

(3) The analogous statements hold for finite products of closed subgroups and of quotients.

Facts & Assumptions

Given: Locally compact Hausdorff abelian groups $G, G_{1}, \dots, G_{n}$ , a closed subgroup $H \leq G$ , and the evaluation maps $Φ_{A} (a) (λ) = λ (a)$ .

[F1]

The product-dual map $Ψ : {\hat{G}}_{1} \times \dots \times {\hat{G}}_{n} \to \hat{G_{1} \times \dots \times G_{n}}$ , $Ψ (γ_{1}, \dots, γ_{n}) (x_{1}, \dots, x_{n}) = \prod_{j} γ_{j} (x_{j})$ , is an isomorphism of topological groups, and it is natural for the projections. The evaluation pairing of the product is computed coordinatewise. (Duals of finite products and of discrete direct sums, 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, 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, The Pontryagin dual with the compact-open topology)

[F2]

Closed subgroups of LCA groups are LCA (A locally compact subgroup of a Hausdorff topological group is closed), as are quotients by closed subgroups (The quotient of an LCA group by a closed subgroup is LCA) and finite products: products inherit continuous operations and the Hausdorff property, and products of compact neighbourhoods give compact neighbourhoods (A product of finitely many compact spaces is compact in the product topology). Their duals are LCA under AC (The dual of a locally compact abelian group is locally compact abelian). For every locally compact Hausdorff abelian group $A$ the evaluation map $Φ_{A} : A \to \hat{\hat{A}}$ is an isomorphism of topological groups. (Pontryagin biduality: the evaluation map is a topological isomorphism)

[F3]

For a closed subgroup $H \leq G$ : restriction $R : \hat{G} \to \hat{H}$ is an open continuous surjection with kernel $H^{⊥}$ inducing $\hat{G} / H^{⊥} ≅ \hat{H}$ ; the pullback $\hat{q}$ of the quotient map $q : G \to G / H$ is a topological isomorphism $\hat{G / H} \to H^{⊥}$ ; and $H^{⊥ ⊥} = H$ under the biduality identification. (The dual of a closed subgroup is a quotient of the dual, The dual of a quotient is the annihilator, Annihilators reverse inclusions and the double annihilator closes the subgroup, Characters of a closed subgroup extend to the ambient LCA group, The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ , The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection, The annihilator of a subgroup)

[F4]

Naturality of evaluation is a direct computation: for a continuous homomorphism $φ : A \to B$ of locally compact Hausdorff abelian groups and all $a \in A$ , $λ \in \hat{B}$ , one has $Φ_{B} (φ (a)) (λ) = λ (φ (a)) = (λ \circ φ) (a) = Φ_{A} (a) (\hat{φ} λ) = (\hat{\hat{φ}} (Φ_{A} (a))) (λ)$ , so $Φ_{B} \circ φ = \hat{\hat{φ}} \circ Φ_{A}$ . (Dual homomorphisms: continuity, and the annihilator of a closed subgroup, The Pontryagin dual with the compact-open topology, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological)

[F5]

The quotient universal property makes the inclusion-induced restriction and the quotient pullback the transposes of the inclusion $H ↪ G$ and of the quotient map $G \to G / H$ respectively. (For a quotient map $q : X \to Y$ , a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$ ; and a composite of quotient maps is a quotient map, Subgroup, The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ )

Proof

1.1F1F2

Part (1): under the identification of the double dual of the product $\hat{\hat{G_{1} \times \dots \times G_{n}}}$ with $\hat{{\hat{G}}_{1}} \times \dots \times \hat{{\hat{G}}_{n}}$ obtained by applying [F1] twice, both $Φ_{G_{1} \times \dots \times G_{n}} (x_{1}, \dots, x_{n})$ and $(Φ_{G_{1}} (x_{1}), \dots, Φ_{G_{n}} (x_{n}))$ are characters of ${\hat{G}}_{1} \times \dots \times {\hat{G}}_{n}$ , and on $(γ_{1}, \dots, γ_{n})$ both take the value $\prod_{j} γ_{j} (x_{j})$ ; hence the two coincide.

2.1F3F4F5step 1.1

Part (2), inclusion: the restriction $R : \hat{G} \to \hat{H}$ is the transpose of the inclusion $ι : H ↪ G$ , so naturality [F4] applied to $ι$ gives $Φ_{G} \circ ι = \hat{R} \circ Φ_{H}$ : for $h \in H$ the character $Φ_{H} (h)$ pulled back along $R$ is $Φ_{G} (h)$ , that is, the two evaluations agree on $H$ .

2.2F3F4F5step 1.1

Part (2), quotient: the pullback $\hat{q} : \hat{G / H} \to \hat{G}$ of the quotient map $q : G \to G / H$ is the transpose of $q$ , so [F4] applied to $q$ gives $Φ_{G / H} \circ q = \hat{\hat{q}} \circ Φ_{G}$ : for $x \in G$ and $η \in \hat{G / H}$ one has $Φ_{G / H} (q (x)) (η) = η (q (x)) = Φ_{G} (x) (η \circ q)$ , so $Φ_{G / H} (x + H)$ is recovered by restricting $Φ_{G} (x)$ to the subgroup $H^{⊥}$ under $\hat{q}$ ; this restriction depends only on the coset $x + H$ .

3.1F3step 2.1step 2.2

Part (2), conclusion: the two naturality identities of steps 2.1 and 2.2 intertwine the exact sequence with its dual, and $H^{⊥ ⊥} = H$ is the closed-subgroup case of [F3].

3.2F1F5step 1.1step 2.1step 2.2

Part (3): for finite products of closed subgroups $H_{j} \leq G_{j}$ the statements follow coordinatewise from part (1) and steps 2.1 and 2.2 applied in each factor; finite products of quotients are handled the same way, since $\prod_{j} (G_{j} / H_{j}) ≅ (\prod_{j} G_{j}) / (\prod_{j} H_{j})$ : the product of the quotient maps is a continuous open surjection (images of basic open rectangles are open rectangles) with kernel $\prod_{j} H_{j}$ , so its induced bijection on the quotient is continuous and open.

4.1step 1.1step 3.1step 3.2∎

Parts (1), (2) and (3) are proved in steps 1.1, 3.1 and 3.2; this is the statement.

Depends on

Used by

Dualisation is a contravariant involution Corollary

Dependency tree · two levels

87 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

T. W. Koerner, Topological Groups (author lecture notes) (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)