Constructive Peter--Weyl Theory: What is Known and What Remains Open

TL;DR

This paper reviews constructive versions of the Peter--Weyl theorem, clarifying which parts are constructively reformulable, which are weaker, and identifying open questions, with a focus on finite-rank approximations and locale-theoretic methods.

Contribution

It provides a comprehensive survey of constructive reformulations of the Peter--Weyl theorem, highlighting the differences from classical versions and outlining open problems.

Findings

Constructive theory exists but differs from classical formulations.

Finite-rank approximation and characters are central in constructive versions.

Classical proofs rely on non-constructive steps, highlighting areas for further research.

Abstract

This survey-style note reviews constructive versions of the Peter--Weyl theorem in the Bishop--Coquand--Spitters line. Its main purpose is to clarify which parts of the classical Peter--Weyl package admit constructive reformulations, which parts survive only in weaker or reorganized form, and which questions still appear to remain open. The term ``constructive'' is used here primarily in the Bishop-style sense, together with the related locale-theoretic and formal-topological developments that occur in the work of Coquand and Spitters. We review the constructive compact-group results of Coquand and Spitters, the later role of almost periodic functions and compact completions, and the interaction with constructive Gelfand representation and locale-theoretic compactness. The guiding theme is that the constructive theory exists, but it is often most naturally expressed not as a literal transcription of the classical theorem in terms of irreducible decompositions alone, but rather through finite-rank approximation, characters, and compactifications attached to functions or groups. For orientation and comparison, we also include an appendix giving a standard classical form of the Peter--Weyl theorem together with a pedagogical Haar-measure-based proof, followed by comments indicating where the classical argument relies on steps that are not automatically constructive. Possible later extensions to topological loops and quasigroups are included as a programmatic direction rather than as part of the currently established core.