Representations of compact groups

TheoremPeter–Weyl theorem: unitary representations separate points#✓fully proved

Let \(G\) be a compact Hausdorff topological group and let \(x \ne y\) be elements of \(G\). Then there are an integer \(n > 0\) and a continuous map \(\rho\) from \(G\) to the complex \(n \times n\) matrices such that \(\rho(1) = 1\), \(\rho(gh) = \rho(g)\rho(h)\) for all \(g, h \in G\), the matrix \(\rho(g)\) is unitary for every \(g \in G\), and \(\rho(x) \ne \rho(y)\).

public theorem peter_weyl_point_separation
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G]
    {x y : G} (hxy : x ≠ y) :
    ∃ (n : ℕ) (_hn : 0 < n) (ρ : G → Matrix (Fin n) (Fin n) ℂ),
      Continuous ρ ∧
      ρ 1 = 1 ∧
      (∀ g h : G, ρ (g * h) = ρ g * ρ h) ∧
      (∀ g : G, ρ g ∈ Matrix.unitaryGroup (Fin n) ℂ) ∧
      ρ x ≠ ρ y

Sources

• F. Peter and H. Weyl, Math. Ann. 97 (1927), 737–755; Folland, A Course in Abstract Harmonic Analysis 2nd ed.; Knapp, Lie Groups Beyond an Introduction 2nd ed.

TheoremRepresentations of compact groups are semisimple#●ready to prove

Let \(G\) be a compact topological group and let \(\rho\) be a representation of \(G\) on a finite-dimensional real normed space \(V\) such that the action map \(G \times V \to V\), \((g, v) \mapsto \rho(g)(v)\), is continuous. Then \(\rho\) is semisimple: every subrepresentation of \(\rho\) has a complementary subrepresentation.

public theorem_wanted compact_group_semisimple
    {G V : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
    (ρ : Representation ℝ G V)
    (hρ : Continuous fun p : G × V => ρ p.1 p.2) :
    ρ.IsSemisimpleRepresentation

Sources

• H. Weyl, Theorie der Darstellung kontinuierlicher halb-einfacher Gruppen durch lineare Transformationen (1925–26); Peter–Weyl (1927). Knill, Some fundamental theorems in mathematics, §21. Problem compact_group_semisimple of the lean-eval benchmark.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.