Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Takao Inoué

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.

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.
Paper Structure (24 sections, 24 theorems, 30 equations, 1 figure)

This paper contains 24 sections, 24 theorems, 30 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Structure of the note
  3. The Classical Peter--Weyl Package
  4. Why Constructive Reformulation Is Needed
  5. Known Constructive Results
  6. Compact groups
  7. Almost periodic functions and compact completions
  8. Locales and constructive Gelfand theory
  9. A Working Dictionary: Classical vs. Constructive
  10. What Seems To Be Established
  11. What Still Seems Open or At Least Insufficiently Clarified
  12. Technical questions inside the current framework
  13. Programmatic questions beyond the present framework
  14. A Programmatic Outlook Toward Loops and Quasigroups
  15. A Suggested Program for Future Work
  16. ...and 9 more sections

Key Result

Theorem 4.1

Let $G$ be a compact group in the constructive setting considered in CoquandSpittersPW. Then there is a directed family of finite-rank operators $P_F$ on the relevant function space, indexed by finite character-theoretic data $F$, such that each $P_F$ is built from convolution with central functions in the constructive mode of approximation used in CoquandSpittersPW. Moreover, the image of each $P

Figures (1)

  • Figure 1: Two routes to constructive Peter--Weyl approximation: a direct compact-group route and an almost-periodic route via compact completion. In both cases the essential structure is not a global decomposition of $L^2(G)$ but a directed family of explicit finite-rank approximation operators $P_F$ whose refinement yields approximation to the original function. This modular pattern provides the template for possible later extensions to non-associative settings.

Theorems & Definitions (54)

  • Remark 2.1
  • Remark 3.1: Foundational stance
  • Theorem 4.1: Coquand--Spitters, schematic operator form
  • proof : Explanation
  • Remark 4.2
  • Proposition 4.3: Finite-stage approximation principle
  • proof
  • Proposition 4.4: Constructive emphasis of the compact-group theory
  • proof
  • Proposition 4.5: Compactification principle, schematic form
  • ...and 44 more