theorem · Pro-C groups

Pontryagin biduality for profinite abelian groups

Evaluation identifies a profinite abelian group with its continuous character bidual.

Finite quotient characters distinguish elements, while compactness allows compatible finite evaluation conditions to be solved simultaneously. The resulting identification preserves both topology and finite torsion, giving a canonical passage between a group and its character data. This is the profinite abelian case of the duality theory developed in Pontrjagin’s 1934 paper on topological commutative groups.

ProCGroups on GitHub ↗

Mathematical statement

Let $G$ be a compact, totally disconnected abelian topological group. Its Pontryagin dual $G^\vee$ consists of continuous circle-valued characters with the compact-open topology. The source constructs a continuous group isomorphism $$G\xrightarrow{\sim}(G^\vee)^\vee,\qquad g\longmapsto\bigl(\chi\longmapsto\chi(g)\bigr).$$

This is an isomorphism of the actual topological groups. In particular, finite torsion is retained; this is not an identification obtained only after tensoring with a field.

Lean code

`ProCGroups.Duality.profiniteBidualEquiv`

Published library source ↗Same source in NYLL ↗

def profiniteBidualEquiv : G ≃ₜ* PontryaginDual (PontryaginDual G)

In-scope Lean context

noncomputable section

open ProCGroups.ProC

namespace ProCGroups.Duality

universe u

variable {G : Type u} [CommGroup G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]

Full declaration and proof

/-- A profinite abelian group is canonically isomorphic, with its actual topology,
to its Pontryagin double dual. This retains all torsion. -/
def profiniteBidualEquiv : G ≃ₜ* PontryaginDual (PontryaginDual G) := by
  let e : G ≃* PontryaginDual (PontryaginDual G) :=
    MulEquiv.ofBijective (bidualEvaluation G).toMonoidHom
      ⟨profinite_bidualEvaluation_injective, profinite_bidualEvaluation_surjective⟩
  exact
    { toMulEquiv := e
      continuous_toFun := (bidualEvaluation G).continuous
      continuous_invFun := (Continuous.homeoOfEquivCompactToT2 (f := e.toEquiv)
        (bidualEvaluation G).continuous).continuous_invFun }

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

L. Pontrjagin. The Theory of Topological Commutative Groups. Annals of Mathematics, 35 (2), 361–388, 1934.

Published source: 7d74e3a9.

← All selected results in Pro-C groups