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

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.