Editing Peter–Weyl theorem (section)

==Consequences==
===Representation theory of connected compact Lie groups===
The Peter–Weyl theorem—specifically the assertion that the characters form an orthonormal ''basis'' for the space of square-integrable class functions—plays a key role in the [[Compact group#Representation theory of a connected compact Lie group|classification]] of the irreducible representations of a connected compact Lie group.<ref>{{harvnb|Hall|2015}} Section 12.5</ref> The argument also depends on the [[Maximal torus#Weyl integral formula|Weyl integral formula]] (for class functions) and the [[Weyl character formula]].

An outline of the argument may be found [[Compact group#An outline of the proof|here]].

===Linearity of compact Lie groups===
One important consequence of the Peter–Weyl theorem is the following:<ref>{{harvnb|Knapp|2002|loc=Corollary IV.4.22}}</ref>
:'''Theorem''': Every compact Lie group has a faithful finite-dimensional representation and is therefore isomorphic to a closed subgroup of <math>\operatorname{GL}(n;\mathbb{C})</math> for some <math>n</math>.

===Structure of compact topological groups===
From the Peter–Weyl theorem, one can deduce a significant general structure theorem. Let ''G'' be a compact topological group, which we assume [[Hausdorff space|Hausdorff]]. For any finite-dimensional ''G''-invariant subspace ''V'' in ''L''<sup>2</sup>(''G''), where ''G'' [[Group action (mathematics)|acts]] on the left, we consider the image of ''G'' in GL(''V''). It is closed, since ''G'' is compact, and a subgroup of the [[Lie group]] GL(''V''). It follows by a [[Closed subgroup theorem|theorem]] of [[Élie Cartan]] that the image of ''G'' is a Lie group also.

If we now take the [[Limit (category theory)|limit]] (in the sense of [[category theory]]) over all such spaces ''V'', we get a result about ''G'': Because ''G'' acts faithfully on ''L''<sup>2</sup>(''G''), ''G'' is an ''inverse limit of Lie groups''. It may of course not itself be a Lie group: it may for example be a [[profinite group]].