Constructive Peter--Weyl Theory: What is Known and What Remains Open
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915871834767360 |
|---|---|
| author | Inoué, Takao |
| author_facet | Inoué, Takao |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_17618 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Constructive Peter--Weyl Theory: What is Known and What Remains Open Inoué, Takao Functional Analysis 43A65, 03F60, 22C05, 46J10 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. |
| title | Constructive Peter--Weyl Theory: What is Known and What Remains Open |
| topic | Functional Analysis 43A65, 03F60, 22C05, 46J10 |
| url | https://arxiv.org/abs/2603.17618 |